From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 22 May 2019 13:43:08 +0200
Subject: htmldoc regenerated
---
.../mathcomp.solvable.primitive_action.html | 89 +++++++++++-----------
1 file changed, 43 insertions(+), 46 deletions(-)
(limited to 'docs/htmldoc/mathcomp.solvable.primitive_action.html')
diff --git a/docs/htmldoc/mathcomp.solvable.primitive_action.html b/docs/htmldoc/mathcomp.solvable.primitive_action.html
index ee8d1dc..fcf9d4a 100644
--- a/docs/htmldoc/mathcomp.solvable.primitive_action.html
+++ b/docs/htmldoc/mathcomp.solvable.primitive_action.html
@@ -21,7 +21,6 @@
@@ -54,15 +53,15 @@
Variables (aT : finGroupType) (sT : finType).
-Variables (A : {set aT}) (S : {set sT}) (to : {action aT &-> sT}).
+Variables (A : {set aT}) (S : {set sT}) (to : {action aT &-> sT}).
Definition imprimitivity_system Q :=
- [&& partition Q S, [acts A, on Q | to^*] & 1 < #|Q| < #|S|].
+ [&& partition Q S, [acts A, on Q | to^*] & 1 < #|Q| < #|S|].
Definition primitive :=
- [transitive A, on S | to] && ~~ [∃ Q, imprimitivity_system Q].
+ [transitive A, on S | to] && ~~ [∃ Q, imprimitivity_system Q].
End PrimitiveDef.
@@ -70,27 +69,25 @@
-Notation "[ 'primitive' A , 'on' S | to ]" := (primitive A S to)
+Notation "[ 'primitive' A , 'on' S | to ]" := (primitive A S to)
(at level 0, format "[ 'primitive' A , 'on' S | to ]") : form_scope.
-
-
Section Primitive.
Variables (aT : finGroupType) (sT : finType).
-Variables (G : {group aT}) (to : {action aT &-> sT}) (S : {set sT}).
+Variables (G : {group aT}) (to : {action aT &-> sT}) (S : {set sT}).
Lemma trans_prim_astab x :
- x \in S → [transitive G, on S | to] →
- [primitive G, on S | to] = maximal_eq 'C_G[x | to] G.
+ x \in S → [transitive G, on S | to] →
+ [primitive G, on S | to] = maximal_eq 'C_G[x | to] G.
-Lemma prim_trans_norm (H : {group aT}) :
- [primitive G, on S | to] → H <| G →
- H \subset 'C_G(S | to) ∨ [transitive H, on S | to].
+Lemma prim_trans_norm (H : {group aT}) :
+ [primitive G, on S | to] → H <| G →
+ H \subset 'C_G(S | to) ∨ [transitive H, on S | to].
End Primitive.
@@ -100,10 +97,10 @@
Variables (gT : finGroupType) (sT : finType).
-Variables (to : {action gT &-> sT}) (n : nat).
+Variables (to : {action gT &-> sT}) (n : nat).
-Definition n_act (t : n.-tuple sT) a := [tuple of map (to^~ a) t].
+Definition n_act (t : n.-tuple sT) a := [tuple of map (to^~ a) t].
Fact n_act_is_action : is_action setT n_act.
@@ -115,26 +112,26 @@
End NactionDef.
-Notation "to * n" := (n_act_action to n) : action_scope.
+Notation "to * n" := (n_act_action to n) : action_scope.
Section NTransitive.
Variables (gT : finGroupType) (sT : finType).
-Variables (n : nat) (A : {set gT}) (S : {set sT}) (to : {action gT &-> sT}).
+Variables (n : nat) (A : {set gT}) (S : {set sT}) (to : {action gT &-> sT}).
-Definition dtuple_on := [set t : n.-tuple sT | uniq t & t \subset S].
-Definition ntransitive := [transitive A, on dtuple_on | to × n].
+Definition dtuple_on := [set t : n.-tuple sT | uniq t & t \subset S].
+Definition ntransitive := [transitive A, on dtuple_on | to × n].
Lemma dtuple_onP t :
- reflect (injective (tnth t) ∧ ∀ i, tnth t i \in S) (t \in dtuple_on).
+ reflect (injective (tnth t) ∧ ∀ i, tnth t i \in S) (t \in dtuple_on).
Lemma n_act_dtuple t a :
- a \in 'N(S | to) → t \in dtuple_on → n_act to t a \in dtuple_on.
+ a \in 'N(S | to) → t \in dtuple_on → n_act to t a \in dtuple_on.
End NTransitive.
@@ -142,11 +139,11 @@
-Notation "n .-dtuple ( S )" := (dtuple_on n S)
+Notation "n .-dtuple ( S )" := (dtuple_on n S)
(at level 8, format "n .-dtuple ( S )") : set_scope.
-Notation "[ 'transitive' ^ n A , 'on' S | to ]" := (ntransitive n A S to)
+Notation "[ 'transitive' ^ n A , 'on' S | to ]" := (ntransitive n A S to)
(at level 0, n at level 8,
format "[ 'transitive' ^ n A , 'on' S | to ]") : form_scope.
@@ -155,46 +152,46 @@
Variables (gT : finGroupType) (sT : finType).
-Variables (to : {action gT &-> sT}) (G : {group gT}) (S : {set sT}).
+Variables (to : {action gT &-> sT}) (G : {group gT}) (S : {set sT}).
-Lemma card_uniq_tuple n (t : n.-tuple sT) : uniq t → #|t| = n.
+Lemma card_uniq_tuple n (t : n.-tuple sT) : uniq t → #|t| = n.
-Lemma n_act0 (t : 0.-tuple sT) a : n_act to t a = [tuple].
+Lemma n_act0 (t : 0.-tuple sT) a : n_act to t a = [tuple].
-Lemma dtuple_on_add n x (t : n.-tuple sT) :
- ([tuple of x :: t] \in n.+1.-dtuple(S)) =
- [&& x \in S, x \notin t & t \in n.-dtuple(S)].
+Lemma dtuple_on_add n x (t : n.-tuple sT) :
+ ([tuple of x :: t] \in n.+1.-dtuple(S)) =
+ [&& x \in S, x \notin t & t \in n.-dtuple(S)].
-Lemma dtuple_on_add_D1 n x (t : n.-tuple sT) :
- ([tuple of x :: t] \in n.+1.-dtuple(S))
- = (x \in S) && (t \in n.-dtuple(S :\ x)).
+Lemma dtuple_on_add_D1 n x (t : n.-tuple sT) :
+ ([tuple of x :: t] \in n.+1.-dtuple(S))
+ = (x \in S) && (t \in n.-dtuple(S :\ x)).
-Lemma dtuple_on_subset n (S1 S2 : {set sT}) t :
- S1 \subset S2 → t \in n.-dtuple(S1) → t \in n.-dtuple(S2).
+Lemma dtuple_on_subset n (S1 S2 : {set sT}) t :
+ S1 \subset S2 → t \in n.-dtuple(S1) → t \in n.-dtuple(S2).
-Lemma n_act_add n x (t : n.-tuple sT) a :
- n_act to [tuple of x :: t] a = [tuple of to x a :: n_act to t a].
+Lemma n_act_add n x (t : n.-tuple sT) a :
+ n_act to [tuple of x :: t] a = [tuple of to x a :: n_act to t a].
-Lemma ntransitive0 : [transitive^0 G, on S | to].
+Lemma ntransitive0 : [transitive^0 G, on S | to].
Lemma ntransitive_weak k m :
- k ≤ m → [transitive^m G, on S | to] → [transitive^k G, on S | to].
+ k ≤ m → [transitive^m G, on S | to] → [transitive^k G, on S | to].
Lemma ntransitive1 m :
- 0 < m → [transitive^m G, on S | to] → [transitive G, on S | to].
+ 0 < m → [transitive^m G, on S | to] → [transitive G, on S | to].
Lemma ntransitive_primitive m :
- 1 < m → [transitive^m G, on S | to] → [primitive G, on S | to].
+ 1 < m → [transitive^m G, on S | to] → [primitive G, on S | to].
End NTransitveProp.
@@ -204,7 +201,7 @@
Variables (gT : finGroupType) (sT : finType).
-Variables (to : {action gT &-> sT}) (G : {group gT}) (S : {set sT}).
+Variables (to : {action gT &-> sT}) (G : {group gT}) (S : {set sT}).
@@ -214,8 +211,8 @@
@@ -225,9 +222,9 @@