-
Notation "''Fix_' ( to ) ( A )" :=
'Fix_to(A)
+
Notation "''Fix_' ( to ) ( A )" :=
'Fix_to(A)
(
at level 8,
only parsing) :
group_scope.
-
Notation "''Fix_' ( S | to ) ( A )" := (
S :&: 'Fix_to(A))
+
Notation "''Fix_' ( S | to ) ( A )" := (
S :&: 'Fix_to(A))
(
at level 8,
format "''Fix_' ( S | to ) ( A )") :
group_scope.
-
Notation "''Fix_' to [ a ]" := (
'Fix_to([set a]))
+
Notation "''Fix_' to [ a ]" := (
'Fix_to([set a]))
(
at level 8,
to at level 2,
format "''Fix_' to [ a ]") :
group_scope.
-
Notation "''Fix_' ( S | to ) [ a ]" := (
S :&: 'Fix_to[a])
+
Notation "''Fix_' ( S | to ) [ a ]" := (
S :&: 'Fix_to[a])
(
at level 8,
format "''Fix_' ( S | to ) [ a ]") :
group_scope.
-
Notation "''C' ( S | to )" := (
astab S to)
+
Notation "''C' ( S | to )" := (
astab S to)
(
at level 8,
format "''C' ( S | to )") :
group_scope.
-
Notation "''C_' A ( S | to )" := (
A :&: 'C(S | to))
+
Notation "''C_' A ( S | to )" := (
A :&: 'C(S | to))
(
at level 8,
A at level 2,
format "''C_' A ( S | to )") :
group_scope.
-
Notation "''C_' ( A ) ( S | to )" :=
'C_A(S | to)
+
Notation "''C_' ( A ) ( S | to )" :=
'C_A(S | to)
(
at level 8,
only parsing) :
group_scope.
-
Notation "''C' [ x | to ]" := (
'C([set x] | to))
+
Notation "''C' [ x | to ]" := (
'C([set x] | to))
(
at level 8,
format "''C' [ x | to ]") :
group_scope.
-
Notation "''C_' A [ x | to ]" := (
A :&: 'C[x | to])
+
Notation "''C_' A [ x | to ]" := (
A :&: 'C[x | to])
(
at level 8,
A at level 2,
format "''C_' A [ x | to ]") :
group_scope.
-
Notation "''C_' ( A ) [ x | to ]" :=
'C_A[x | to]
+
Notation "''C_' ( A ) [ x | to ]" :=
'C_A[x | to]
(
at level 8,
only parsing) :
group_scope.
-
Notation "''N' ( S | to )" := (
astabs S to)
+
Notation "''N' ( S | to )" := (
astabs S to)
(
at level 8,
format "''N' ( S | to )") :
group_scope.
-
Notation "''N_' A ( S | to )" := (
A :&: 'N(S | to))
+
Notation "''N_' A ( S | to )" := (
A :&: 'N(S | to))
(
at level 8,
A at level 2,
format "''N_' A ( S | to )") :
group_scope.
-
Notation "[ 'acts' A , 'on' S | to ]" := (
A \subset pred_of_set 'N(S | to))
+
Notation "[ 'acts' A , 'on' S | to ]" := (
A \subset pred_of_set 'N(S | to))
(
at level 0,
format "[ 'acts' A , 'on' S | to ]") :
form_scope.
-
Notation "{ 'acts' A , 'on' S | to }" := (
acts_on A S to)
+
Notation "{ 'acts' A , 'on' S | to }" := (
acts_on A S to)
(
at level 0,
format "{ 'acts' A , 'on' S | to }") :
form_scope.
-
Notation "[ 'transitive' A , 'on' S | to ]" := (
atrans A S to)
+
Notation "[ 'transitive' A , 'on' S | to ]" := (
atrans A S to)
(
at level 0,
format "[ 'transitive' A , 'on' S | to ]") :
form_scope.
-
Notation "[ 'faithful' A , 'on' S | to ]" := (
faithful A S to)
+
Notation "[ 'faithful' A , 'on' S | to ]" := (
faithful A S to)
(
at level 0,
format "[ 'faithful' A , 'on' S | to ]") :
form_scope.
@@ -348,158 +347,158 @@
-
Variables (
aT :
finGroupType) (
D :
{set aT}) (
rT :
finType) (
to :
action D rT).
+
Variables (
aT :
finGroupType) (
D :
{set aT}) (
rT :
finType) (
to :
action D rT).
-
Implicit Types (
a :
aT) (
x y :
rT) (
A B :
{set aT}) (
S T :
{set rT}).
+
Implicit Types (
a :
aT) (
x y :
rT) (
A B :
{set aT}) (
S T :
{set rT}).
-
Lemma act_inj :
left_injective to.
+
Lemma act_inj :
left_injective to.
-
Lemma actMin x :
{in D &, act_morph to x}.
+
Lemma actMin x :
{in D &, act_morph to x}.
-
Lemma actmEfun a :
a \in D → actm to a = to^~ a.
+
Lemma actmEfun a :
a \in D → actm to a = to^~ a.
-
Lemma actmE a :
a \in D → actm to a =1 to^~ a.
+
Lemma actmE a :
a \in D → actm to a =1 to^~ a.
-
Lemma setactE S a :
to^* S a = [set to x a | x in S].
+
Lemma setactE S a :
to^* S a = [set to x a | x in S].
-
Lemma mem_setact S a x :
x \in S → to x a \in to^* S a.
+
Lemma mem_setact S a x :
x \in S → to x a \in to^* S a.
-
Lemma card_setact S a :
#|to^* S a| = #|S|.
+
Lemma card_setact S a :
#|to^* S a| = #|S|.
-
Lemma setact_is_action :
is_action D to^*.
+
Lemma setact_is_action :
is_action D to^*.
Canonical set_action :=
Action setact_is_action.
-
Lemma orbitE A x :
orbit to A x = to x @: A.
+
Lemma orbitE A x :
orbit to A x = to x @: A.
Lemma orbitP A x y :
-
reflect (
exists2 a, a \in A & to x a = y) (
y \in orbit to A x).
+
reflect (
exists2 a, a \in A & to x a = y) (
y \in orbit to A x).
-
Lemma mem_orbit A x a :
a \in A → to x a \in orbit to A x.
+
Lemma mem_orbit A x a :
a \in A → to x a \in orbit to A x.
-
Lemma afixP A x :
reflect (
∀ a,
a \in A → to x a = x) (
x \in 'Fix_to(A)).
+
Lemma afixP A x :
reflect (
∀ a,
a \in A → to x a = x) (
x \in 'Fix_to(A)).
-
Lemma afixS A B :
A \subset B → 'Fix_to(B) \subset 'Fix_to(A).
+
Lemma afixS A B :
A \subset B → 'Fix_to(B) \subset 'Fix_to(A).
-
Lemma afixU A B :
'Fix_to(A :|: B) = 'Fix_to(A) :&: 'Fix_to(B).
+
Lemma afixU A B :
'Fix_to(A :|: B) = 'Fix_to(A) :&: 'Fix_to(B).
-
Lemma afix1P a x :
reflect (
to x a = x) (
x \in 'Fix_to[a]).
+
Lemma afix1P a x :
reflect (
to x a = x) (
x \in 'Fix_to[a]).
-
Lemma astabIdom S :
'C_D(S | to) = 'C(S | to).
+
Lemma astabIdom S :
'C_D(S | to) = 'C(S | to).
-
Lemma astab_dom S :
{subset 'C(S | to) ≤ D}.
+
Lemma astab_dom S :
{subset 'C(S | to) ≤ D}.
-
Lemma astab_act S a x :
a \in 'C(S | to) → x \in S → to x a = x.
+
Lemma astab_act S a x :
a \in 'C(S | to) → x \in S → to x a = x.
-
Lemma astabS S1 S2 :
S1 \subset S2 → 'C(S2 | to) \subset 'C(S1 | to).
+
Lemma astabS S1 S2 :
S1 \subset S2 → 'C(S2 | to) \subset 'C(S1 | to).
-
Lemma astabsIdom S :
'N_D(S | to) = 'N(S | to).
+
Lemma astabsIdom S :
'N_D(S | to) = 'N(S | to).
-
Lemma astabs_dom S :
{subset 'N(S | to) ≤ D}.
+
Lemma astabs_dom S :
{subset 'N(S | to) ≤ D}.
-
Lemma astabs_act S a x :
a \in 'N(S | to) → (to x a \in S) = (x \in S).
+
Lemma astabs_act S a x :
a \in 'N(S | to) → (to x a \in S) = (x \in S).
-
Lemma astab_sub S :
'C(S | to) \subset 'N(S | to).
+
Lemma astab_sub S :
'C(S | to) \subset 'N(S | to).
-
Lemma astabsC S :
'N(~: S | to) = 'N(S | to).
+
Lemma astabsC S :
'N(~: S | to) = 'N(S | to).
-
Lemma astabsI S T :
'N(S | to) :&: 'N(T | to) \subset 'N(S :&: T | to).
+
Lemma astabsI S T :
'N(S | to) :&: 'N(T | to) \subset 'N(S :&: T | to).
-
Lemma astabs_setact S a :
a \in 'N(S | to) → to^* S a = S.
+
Lemma astabs_setact S a :
a \in 'N(S | to) → to^* S a = S.
-
Lemma astab1_set S :
'C[S | set_action] = 'N(S | to).
+
Lemma astab1_set S :
'C[S | set_action] = 'N(S | to).
-
Lemma astabs_set1 x :
'N([set x] | to) = 'C[x | to].
+
Lemma astabs_set1 x :
'N([set x] | to) = 'C[x | to].
-
Lemma acts_dom A S :
[acts A, on S | to] → A \subset D.
+
Lemma acts_dom A S :
[acts A, on S | to] → A \subset D.
-
Lemma acts_act A S :
[acts A, on S | to] → {acts A, on S | to}.
+
Lemma acts_act A S :
[acts A, on S | to] → {acts A, on S | to}.
Lemma astabCin A S :
-
A \subset D → (A \subset 'C(S | to)) = (S \subset 'Fix_to(A)).
+
A \subset D → (A \subset 'C(S | to)) = (S \subset 'Fix_to(A)).
Section ActsSetop.
-
Variables (
A :
{set aT}) (
S T :
{set rT}).
-
Hypotheses (
AactS :
[acts A, on S | to]) (
AactT :
[acts A, on T | to]).
+
Variables (
A :
{set aT}) (
S T :
{set rT}).
+
Hypotheses (
AactS :
[acts A, on S | to]) (
AactT :
[acts A, on T | to]).
-
Lemma astabU :
'C(S :|: T | to) = 'C(S | to) :&: 'C(T | to).
+
Lemma astabU :
'C(S :|: T | to) = 'C(S | to) :&: 'C(T | to).
-
Lemma astabsU :
'N(S | to) :&: 'N(T | to) \subset 'N(S :|: T | to).
+
Lemma astabsU :
'N(S | to) :&: 'N(T | to) \subset 'N(S :|: T | to).
-
Lemma astabsD :
'N(S | to) :&: 'N(T | to) \subset 'N(S :\: T| to).
+
Lemma astabsD :
'N(S | to) :&: 'N(T | to) \subset 'N(S :\: T| to).
-
Lemma actsI :
[acts A, on S :&: T | to].
+
Lemma actsI :
[acts A, on S :&: T | to].
-
Lemma actsU :
[acts A, on S :|: T | to].
+
Lemma actsU :
[acts A, on S :|: T | to].
-
Lemma actsD :
[acts A, on S :\: T | to].
+
Lemma actsD :
[acts A, on S :\: T | to].
End ActsSetop.
Lemma acts_in_orbit A S x y :
-
[acts A, on S | to] → y \in orbit to A x → x \in S → y \in S.
+
[acts A, on S | to] → y \in orbit to A x → x \in S → y \in S.
Lemma subset_faithful A B S :
-
B \subset A → [faithful A, on S | to] → [faithful B, on S | to].
+
B \subset A → [faithful A, on S | to] → [faithful B, on S | to].
Section Reindex.
-
Variables (
vT :
Type) (
idx :
vT) (
op :
Monoid.com_law idx) (
S :
{set rT}).
+
Variables (
vT :
Type) (
idx :
vT) (
op :
Monoid.com_law idx) (
S :
{set rT}).
-
Lemma reindex_astabs a F :
a \in 'N(S | to) →
-
\big[op/idx]_(i in S) F i = \big[op/idx]_(i in S) F (
to i a).
+
Lemma reindex_astabs a F :
a \in 'N(S | to) →
+
\big[op/idx]_(i in S) F i = \big[op/idx]_(i in S) F (
to i a).
-
Lemma reindex_acts A a F :
[acts A, on S | to] → a \in A →
-
\big[op/idx]_(i in S) F i = \big[op/idx]_(i in S) F (
to i a).
+
Lemma reindex_acts A a F :
[acts A, on S | to] → a \in A →
+
\big[op/idx]_(i in S) F i = \big[op/idx]_(i in S) F (
to i a).
End Reindex.
@@ -508,16 +507,9 @@
End RawAction.
-
-
-
- Warning: this directive depends on names of bound variables in the
- definition of injective, in ssrfun.v.
-
-
-
Notation "to ^*" := (
set_action to) :
action_scope.
+
Notation "to ^*" := (
set_action to) :
action_scope.
@@ -533,233 +525,233 @@
-
Variables (
aT :
finGroupType) (
D :
{group aT}) (
rT :
finType).
+
Variables (
aT :
finGroupType) (
D :
{group aT}) (
rT :
finType).
Variable to :
action D rT.
Implicit Types a :
aT.
Implicit Types x y :
rT.
-
Implicit Types A B :
{set aT}.
-
Implicit Types G H :
{group aT}.
-
Implicit Types S :
{set rT}.
+
Implicit Types A B :
{set aT}.
+
Implicit Types G H :
{group aT}.
+
Implicit Types S :
{set rT}.
-
Lemma act1 x :
to x 1
= x.
+
Lemma act1 x :
to x 1
= x.
-
Lemma actKin :
{in D, right_loop invg to}.
+
Lemma actKin :
{in D, right_loop invg to}.
-
Lemma actKVin :
{in D, rev_right_loop invg to}.
+
Lemma actKVin :
{in D, rev_right_loop invg to}.
-
Lemma setactVin S a :
a \in D → to^* S a^-1 = to^~ a @^-1: S.
+
Lemma setactVin S a :
a \in D → to^* S a^-1 = to^~ a @^-1: S.
-
Lemma actXin x a i :
a \in D → to x (
a ^+ i)
= iter i (
to^~ a)
x.
+
Lemma actXin x a i :
a \in D → to x (
a ^+ i)
= iter i (
to^~ a)
x.
-
Lemma afix1 :
'Fix_to(1
) = setT.
+
Lemma afix1 :
'Fix_to(1
) = setT.
-
Lemma afixD1 G :
'Fix_to(G^#) = 'Fix_to(G).
+
Lemma afixD1 G :
'Fix_to(G^#) = 'Fix_to(G).
-
Lemma orbit_refl G x :
x \in orbit to G x.
+
Lemma orbit_refl G x :
x \in orbit to G x.
-
Lemma contra_orbit G x y :
x \notin orbit to G y → x != y.
+
Lemma contra_orbit G x y :
x \notin orbit to G y → x != y.
-
Lemma orbit_in_sym G :
G \subset D → symmetric (
orbit_rel G).
+
Lemma orbit_in_sym G :
G \subset D → symmetric (
orbit_rel G).
-
Lemma orbit_in_trans G :
G \subset D → transitive (
orbit_rel G).
+
Lemma orbit_in_trans G :
G \subset D → transitive (
orbit_rel G).
Lemma orbit_in_eqP G x y :
-
G \subset D → reflect (
orbit to G x = orbit to G y) (
x \in orbit to G y).
+
G \subset D → reflect (
orbit to G x = orbit to G y) (
x \in orbit to G y).
Lemma orbit_in_transl G x y z :
-
G \subset D → y \in orbit to G x →
-
(y \in orbit to G z) = (x \in orbit to G z).
+
G \subset D → y \in orbit to G x →
+
(y \in orbit to G z) = (x \in orbit to G z).
Lemma orbit_act_in x a G :
-
G \subset D → a \in G → orbit to G (
to x a)
= orbit to G x.
+
G \subset D → a \in G → orbit to G (
to x a)
= orbit to G x.
Lemma orbit_actr_in x a G y :
-
G \subset D → a \in G → (to y a \in orbit to G x) = (y \in orbit to G x).
+
G \subset D → a \in G → (to y a \in orbit to G x) = (y \in orbit to G x).
Lemma orbit_inv_in A x y :
-
A \subset D → (y \in orbit to A^-1 x) = (x \in orbit to A y).
+
A \subset D → (y \in orbit to A^-1 x) = (x \in orbit to A y).
Lemma orbit_lcoset_in A a x :
-
A \subset D → a \in D →
-
orbit to (
a *: A)
x = orbit to A (
to x a).
+
A \subset D → a \in D →
+
orbit to (
a *: A)
x = orbit to A (
to x a).
Lemma orbit_rcoset_in A a x y :
-
A \subset D → a \in D →
-
(to y a \in orbit to (
A :* a)
x) = (y \in orbit to A x).
+
A \subset D → a \in D →
+
(to y a \in orbit to (
A :* a)
x) = (y \in orbit to A x).
Lemma orbit_conjsg_in A a x y :
-
A \subset D → a \in D →
-
(to y a \in orbit to (
A :^ a) (
to x a)
) = (y \in orbit to A x).
+
A \subset D → a \in D →
+
(to y a \in orbit to (
A :^ a) (
to x a)
) = (y \in orbit to A x).
-
Lemma orbit1P G x :
reflect (
orbit to G x = [set x]) (
x \in 'Fix_to(G)).
+
Lemma orbit1P G x :
reflect (
orbit to G x = [set x]) (
x \in 'Fix_to(G)).
-
Lemma card_orbit1 G x :
#|orbit to G x| = 1%
N → orbit to G x = [set x].
+
Lemma card_orbit1 G x :
#|orbit to G x| = 1%
N → orbit to G x = [set x].
Lemma orbit_partition G S :
-
[acts G, on S | to] → partition (
orbit to G @: S)
S.
+
[acts G, on S | to] → partition (
orbit to G @: S)
S.
-
Definition orbit_transversal A S :=
transversal (
orbit to A @: S)
S.
+
Definition orbit_transversal A S :=
transversal (
orbit to A @: S)
S.
-
Lemma orbit_transversalP G S (
P :=
orbit to G @: S)
+
Lemma orbit_transversalP G S (
P :=
orbit to G @: S)
(
X :=
orbit_transversal G S) :
-
[acts G, on S | to] →
-
[/\ is_transversal X P S, X \subset S,
-
{in X &, ∀ x y,
(y \in orbit to G x) = (x == y)}
-
& ∀ x,
x \in S → exists2 a, a \in G & to x a \in X].
+
[acts G, on S | to] →
+
[/\ is_transversal X P S, X \subset S,
+
{in X &, ∀ x y,
(y \in orbit to G x) = (x == y)}
+
& ∀ x,
x \in S → exists2 a, a \in G & to x a \in X].
-
Lemma group_set_astab S :
group_set 'C(S | to).
+
Lemma group_set_astab S :
group_set 'C(S | to).
Canonical astab_group S :=
group (
group_set_astab S).
-
Lemma afix_gen_in A :
A \subset D → 'Fix_to(<<A>>) = 'Fix_to(A).
+
Lemma afix_gen_in A :
A \subset D → 'Fix_to(<<A>>) = 'Fix_to(A).
-
Lemma afix_cycle_in a :
a \in D → 'Fix_to(<[a]>) = 'Fix_to[a].
+
Lemma afix_cycle_in a :
a \in D → 'Fix_to(<[a]>) = 'Fix_to[a].
Lemma afixYin A B :
-
A \subset D → B \subset D → 'Fix_to(A <*> B) = 'Fix_to(A) :&: 'Fix_to(B).
+
A \subset D → B \subset D → 'Fix_to(A <*> B) = 'Fix_to(A) :&: 'Fix_to(B).
Lemma afixMin G H :
-
G \subset D → H \subset D → 'Fix_to(G × H) = 'Fix_to(G) :&: 'Fix_to(H).
+
G \subset D → H \subset D → 'Fix_to(G × H) = 'Fix_to(G) :&: 'Fix_to(H).
Lemma sub_astab1_in A x :
-
A \subset D → (A \subset 'C[x | to]) = (x \in 'Fix_to(A)).
+
A \subset D → (A \subset 'C[x | to]) = (x \in 'Fix_to(A)).
-
Lemma group_set_astabs S :
group_set 'N(S | to).
+
Lemma group_set_astabs S :
group_set 'N(S | to).
Canonical astabs_group S :=
group (
group_set_astabs S).
-
Lemma astab_norm S :
'N(S | to) \subset 'N('C(S | to)).
+
Lemma astab_norm S :
'N(S | to) \subset 'N('C(S | to)).
-
Lemma astab_normal S :
'C(S | to) <| 'N(S | to).
+
Lemma astab_normal S :
'C(S | to) <| 'N(S | to).
Lemma acts_sub_orbit G S x :
-
[acts G, on S | to] → (orbit to G x \subset S) = (x \in S).
+
[acts G, on S | to] → (orbit to G x \subset S) = (x \in S).
-
Lemma acts_orbit G x :
G \subset D → [acts G, on orbit to G x | to].
+
Lemma acts_orbit G x :
G \subset D → [acts G, on orbit to G x | to].
-
Lemma acts_subnorm_fix A :
[acts 'N_D(A), on 'Fix_to(D :&: A) | to].
+
Lemma acts_subnorm_fix A :
[acts 'N_D(A), on 'Fix_to(D :&: A) | to].
-
Lemma atrans_orbit G x :
[transitive G, on orbit to G x | to].
+
Lemma atrans_orbit G x :
[transitive G, on orbit to G x | to].
Section OrbitStabilizer.
-
Variables (
G :
{group aT}) (
x :
rT).
-
Hypothesis sGD :
G \subset D.
+
Variables (
G :
{group aT}) (
x :
rT).
+
Hypothesis sGD :
G \subset D.
Let ssGD :=
subsetP sGD.
-
Lemma amove_act a :
a \in G → amove to G x (
to x a)
= 'C_G[x | to] :* a.
+
Lemma amove_act a :
a \in G → amove to G x (
to x a)
= 'C_G[x | to] :* a.
-
Lemma amove_orbit :
amove to G x @: orbit to G x = rcosets 'C_G[x | to] G.
+
Lemma amove_orbit :
amove to G x @: orbit to G x = rcosets 'C_G[x | to] G.
Lemma amoveK :
-
{in orbit to G x, cancel (
amove to G x) (
fun Ca ⇒
to x (
repr Ca))
}.
+
{in orbit to G x, cancel (
amove to G x) (
fun Ca ⇒
to x (
repr Ca))
}.
Lemma orbit_stabilizer :
-
orbit to G x = [set to x (
repr Ca)
| Ca in rcosets 'C_G[x | to] G].
+
orbit to G x = [set to x (
repr Ca)
| Ca in rcosets 'C_G[x | to] G].
Lemma act_reprK :
-
{in rcosets 'C_G[x | to] G, cancel (
to x \o repr) (
amove to G x)
}.
+
{in rcosets 'C_G[x | to] G, cancel (
to x \o repr) (
amove to G x)
}.
End OrbitStabilizer.
-
Lemma card_orbit_in G x :
G \subset D → #|orbit to G x| = #|G : 'C_G[x | to]|.
+
Lemma card_orbit_in G x :
G \subset D → #|orbit to G x| = #|G : 'C_G[x | to]|.
Lemma card_orbit_in_stab G x :
-
G \subset D → (
#|orbit to G x| × #|'C_G[x | to]|)%
N = #|G|.
+
G \subset D → (
#|orbit to G x| × #|'C_G[x | to]|)%
N = #|G|.
Lemma acts_sum_card_orbit G S :
-
[acts G, on S | to] → \sum_(T in orbit to G @: S) #|T| = #|S|.
+
[acts G, on S | to] → \sum_(T in orbit to G @: S) #|T| = #|S|.
-
Lemma astab_setact_in S a :
a \in D → 'C(to^* S a | to) = 'C(S | to) :^ a.
+
Lemma astab_setact_in S a :
a \in D → 'C(to^* S a | to) = 'C(S | to) :^ a.
-
Lemma astab1_act_in x a :
a \in D → 'C[to x a | to] = 'C[x | to] :^ a.
+
Lemma astab1_act_in x a :
a \in D → 'C[to x a | to] = 'C[x | to] :^ a.
-
Theorem Frobenius_Cauchy G S :
[acts G, on S | to] →
-
\sum_(a in G) #|'Fix_(S | to)[a]| = (
#|orbit to G @: S| × #|G|)%
N.
+
Theorem Frobenius_Cauchy G S :
[acts G, on S | to] →
+
\sum_(a in G) #|'Fix_(S | to)[a]| = (
#|orbit to G @: S| × #|G|)%
N.
Lemma atrans_dvd_index_in G S :
-
G \subset D → [transitive G, on S | to] → #|S| %| #|G : 'C_G(S | to)|.
+
G \subset D → [transitive G, on S | to] → #|S| %| #|G : 'C_G(S | to)|.
Lemma atrans_dvd_in G S :
-
G \subset D → [transitive G, on S | to] → #|S| %| #|G|.
+
G \subset D → [transitive G, on S | to] → #|S| %| #|G|.
Lemma atransPin G S :
-
G \subset D → [transitive G, on S | to] →
-
∀ x,
x \in S → orbit to G x = S.
+
G \subset D → [transitive G, on S | to] →
+
∀ x,
x \in S → orbit to G x = S.
Lemma atransP2in G S :
-
G \subset D → [transitive G, on S | to] →
-
{in S &, ∀ x y,
exists2 a, a \in G & y = to x a}.
+
G \subset D → [transitive G, on S | to] →
+
{in S &, ∀ x y,
exists2 a, a \in G & y = to x a}.
Lemma atrans_acts_in G S :
-
G \subset D → [transitive G, on S | to] → [acts G, on S | to].
+
G \subset D → [transitive G, on S | to] → [acts G, on S | to].
Lemma subgroup_transitivePin G H S x :
-
x \in S → H \subset G → G \subset D → [transitive G, on S | to] →
-
reflect (
'C_G[x | to] × H = G)
[transitive H, on S | to].
+
x \in S → H \subset G → G \subset D → [transitive G, on S | to] →
+
reflect (
'C_G[x | to] × H = G)
[transitive H, on S | to].
End PartialAction.
@@ -767,16 +759,16 @@
-
Notation "''C' ( S | to )" := (
astab_group to S) :
Group_scope.
-
Notation "''C_' A ( S | to )" := (
setI_group A 'C(S | to)) :
Group_scope.
-
Notation "''C_' ( A ) ( S | to )" := (
setI_group A 'C(S | to))
+
Notation "''C' ( S | to )" := (
astab_group to S) :
Group_scope.
+
Notation "''C_' A ( S | to )" := (
setI_group A 'C(S | to)) :
Group_scope.
+
Notation "''C_' ( A ) ( S | to )" := (
setI_group A 'C(S | to))
(
only parsing) :
Group_scope.
-
Notation "''C' [ x | to ]" := (
astab_group to [set x%
g]) :
Group_scope.
-
Notation "''C_' A [ x | to ]" := (
setI_group A 'C[x | to]) :
Group_scope.
-
Notation "''C_' ( A ) [ x | to ]" := (
setI_group A 'C[x | to])
+
Notation "''C' [ x | to ]" := (
astab_group to [set x%
g]) :
Group_scope.
+
Notation "''C_' A [ x | to ]" := (
setI_group A 'C[x | to]) :
Group_scope.
+
Notation "''C_' ( A ) [ x | to ]" := (
setI_group A 'C[x | to])
(
only parsing) :
Group_scope.
-
Notation "''N' ( S | to )" := (
astabs_group to S) :
Group_scope.
-
Notation "''N_' A ( S | to )" := (
setI_group A 'N(S | to)) :
Group_scope.
+
Notation "''N' ( S | to )" := (
astabs_group to S) :
Group_scope.
+
Notation "''N_' A ( S | to )" := (
setI_group A 'N(S | to)) :
Group_scope.
Section TotalActions.
@@ -791,139 +783,139 @@
Variable (
aT :
finGroupType) (
rT :
finType).
-
Variable to :
{action aT &-> rT}.
+
Variable to :
{action aT &-> rT}.
-
Implicit Types (
a b :
aT) (
x y z :
rT) (
A B :
{set aT}) (
G H :
{group aT}).
-
Implicit Type S :
{set rT}.
+
Implicit Types (
a b :
aT) (
x y z :
rT) (
A B :
{set aT}) (
G H :
{group aT}).
+
Implicit Type S :
{set rT}.
-
Lemma actM x a b :
to x (
a × b)
= to (
to x a)
b.
+
Lemma actM x a b :
to x (
a × b)
= to (
to x a)
b.
-
Lemma actK :
right_loop invg to.
+
Lemma actK :
right_loop invg to.
-
Lemma actKV :
rev_right_loop invg to.
+
Lemma actKV :
rev_right_loop invg to.
-
Lemma actX x a n :
to x (
a ^+ n)
= iter n (
to^~ a)
x.
+
Lemma actX x a n :
to x (
a ^+ n)
= iter n (
to^~ a)
x.
-
Lemma actCJ a b x :
to (
to x a)
b = to (
to x b) (
a ^ b).
+
Lemma actCJ a b x :
to (
to x a)
b = to (
to x b) (
a ^ b).
-
Lemma actCJV a b x :
to (
to x a)
b = to (
to x (
b ^ a^-1))
a.
+
Lemma actCJV a b x :
to (
to x a)
b = to (
to x (
b ^ a^-1))
a.
-
Lemma orbit_sym G x y :
(x \in orbit to G y) = (y \in orbit to G x).
+
Lemma orbit_sym G x y :
(x \in orbit to G y) = (y \in orbit to G x).
Lemma orbit_trans G x y z :
-
x \in orbit to G y → y \in orbit to G z → x \in orbit to G z.
+
x \in orbit to G y → y \in orbit to G z → x \in orbit to G z.
Lemma orbit_eqP G x y :
-
reflect (
orbit to G x = orbit to G y) (
x \in orbit to G y).
+
reflect (
orbit to G x = orbit to G y) (
x \in orbit to G y).
Lemma orbit_transl G x y z :
-
y \in orbit to G x → (y \in orbit to G z) = (x \in orbit to G z).
+
y \in orbit to G x → (y \in orbit to G z) = (x \in orbit to G z).
-
Lemma orbit_act G a x:
a \in G → orbit to G (
to x a)
= orbit to G x.
+
Lemma orbit_act G a x:
a \in G → orbit to G (
to x a)
= orbit to G x.
Lemma orbit_actr G a x y :
-
a \in G → (to y a \in orbit to G x) = (y \in orbit to G x).
+
a \in G → (to y a \in orbit to G x) = (y \in orbit to G x).
Lemma orbit_eq_mem G x y :
-
(orbit to G x == orbit to G y) = (x \in orbit to G y).
+
(orbit to G x == orbit to G y) = (x \in orbit to G y).
-
Lemma orbit_inv A x y :
(y \in orbit to A^-1 x) = (x \in orbit to A y).
+
Lemma orbit_inv A x y :
(y \in orbit to A^-1 x) = (x \in orbit to A y).
-
Lemma orbit_lcoset A a x :
orbit to (
a *: A)
x = orbit to A (
to x a).
+
Lemma orbit_lcoset A a x :
orbit to (
a *: A)
x = orbit to A (
to x a).
Lemma orbit_rcoset A a x y :
-
(to y a \in orbit to (
A :* a)
x) = (y \in orbit to A x).
+
(to y a \in orbit to (
A :* a)
x) = (y \in orbit to A x).
Lemma orbit_conjsg A a x y :
-
(to y a \in orbit to (
A :^ a) (
to x a)
) = (y \in orbit to A x).
+
(to y a \in orbit to (
A :^ a) (
to x a)
) = (y \in orbit to A x).
-
Lemma astabP S a :
reflect (
∀ x,
x \in S → to x a = x) (
a \in 'C(S | to)).
+
Lemma astabP S a :
reflect (
∀ x,
x \in S → to x a = x) (
a \in 'C(S | to)).
-
Lemma astab1P x a :
reflect (
to x a = x) (
a \in 'C[x | to]).
+
Lemma astab1P x a :
reflect (
to x a = x) (
a \in 'C[x | to]).
-
Lemma sub_astab1 A x :
(A \subset 'C[x | to]) = (x \in 'Fix_to(A)).
+
Lemma sub_astab1 A x :
(A \subset 'C[x | to]) = (x \in 'Fix_to(A)).
-
Lemma astabC A S :
(A \subset 'C(S | to)) = (S \subset 'Fix_to(A)).
+
Lemma astabC A S :
(A \subset 'C(S | to)) = (S \subset 'Fix_to(A)).
-
Lemma afix_cycle a :
'Fix_to(<[a]>) = 'Fix_to[a].
+
Lemma afix_cycle a :
'Fix_to(<[a]>) = 'Fix_to[a].
-
Lemma afix_gen A :
'Fix_to(<<A>>) = 'Fix_to(A).
+
Lemma afix_gen A :
'Fix_to(<<A>>) = 'Fix_to(A).
-
Lemma afixM G H :
'Fix_to(G × H) = 'Fix_to(G) :&: 'Fix_to(H).
+
Lemma afixM G H :
'Fix_to(G × H) = 'Fix_to(G) :&: 'Fix_to(H).
Lemma astabsP S a :
-
reflect (
∀ x,
(to x a \in S) = (x \in S)) (
a \in 'N(S | to)).
+
reflect (
∀ x,
(to x a \in S) = (x \in S)) (
a \in 'N(S | to)).
-
Lemma card_orbit G x :
#|orbit to G x| = #|G : 'C_G[x | to]|.
+
Lemma card_orbit G x :
#|orbit to G x| = #|G : 'C_G[x | to]|.
-
Lemma dvdn_orbit G x :
#|orbit to G x| %| #|G|.
+
Lemma dvdn_orbit G x :
#|orbit to G x| %| #|G|.
-
Lemma card_orbit_stab G x : (
#|orbit to G x| × #|'C_G[x | to]|)%
N = #|G|.
+
Lemma card_orbit_stab G x : (
#|orbit to G x| × #|'C_G[x | to]|)%
N = #|G|.
-
Lemma actsP A S :
reflect {acts A, on S | to} [acts A, on S | to].
+
Lemma actsP A S :
reflect {acts A, on S | to} [acts A, on S | to].
-
Lemma setact_orbit A x b :
to^* (
orbit to A x)
b = orbit to (
A :^ b) (
to x b).
+
Lemma setact_orbit A x b :
to^* (
orbit to A x)
b = orbit to (
A :^ b) (
to x b).
-
Lemma astab_setact S a :
'C(to^* S a | to) = 'C(S | to) :^ a.
+
Lemma astab_setact S a :
'C(to^* S a | to) = 'C(S | to) :^ a.
-
Lemma astab1_act x a :
'C[to x a | to] = 'C[x | to] :^ a.
+
Lemma astab1_act x a :
'C[to x a | to] = 'C[x | to] :^ a.
-
Lemma atransP G S :
[transitive G, on S | to] →
-
∀ x,
x \in S → orbit to G x = S.
+
Lemma atransP G S :
[transitive G, on S | to] →
+
∀ x,
x \in S → orbit to G x = S.
-
Lemma atransP2 G S :
[transitive G, on S | to] →
-
{in S &, ∀ x y,
exists2 a, a \in G & y = to x a}.
+
Lemma atransP2 G S :
[transitive G, on S | to] →
+
{in S &, ∀ x y,
exists2 a, a \in G & y = to x a}.
-
Lemma atrans_acts G S :
[transitive G, on S | to] → [acts G, on S | to].
+
Lemma atrans_acts G S :
[transitive G, on S | to] → [acts G, on S | to].
Lemma atrans_supgroup G H S :
-
G \subset H → [transitive G, on S | to] →
-
[transitive H, on S | to] = [acts H, on S | to].
+
G \subset H → [transitive G, on S | to] →
+
[transitive H, on S | to] = [acts H, on S | to].
Lemma atrans_acts_card G S :
-
[transitive G, on S | to] =
-
[acts G, on S | to] && (#|orbit to G @: S| == 1%
N).
+
[transitive G, on S | to] =
+
[acts G, on S | to] && (#|orbit to G @: S| == 1%
N).
-
Lemma atrans_dvd G S :
[transitive G, on S | to] → #|S| %| #|G|.
+
Lemma atrans_dvd G S :
[transitive G, on S | to] → #|S| %| #|G|.
@@ -932,12 +924,12 @@
This is Aschbacher (5.2)
@@ -947,7 +939,7 @@
-
Variables (
aT :
finGroupType) (
D :
{set aT}) (
rT :
finType).
+
Variables (
aT :
finGroupType) (
D :
{set aT}) (
rT :
finType).
Variable to :
action D rT.
Definition actperm a :=
perm (
act_inj to a).
-
Lemma actpermM :
{in D &, {morph actperm : a b / a × b}}.
+
Lemma actpermM :
{in D &, {morph actperm : a b / a × b}}.
Canonical actperm_morphism :=
Morphism actpermM.
-
Lemma actpermE a x :
actperm a x = to x a.
+
Lemma actpermE a x :
actperm a x = to x a.
-
Lemma actpermK x a :
aperm x (
actperm a)
= to x a.
+
Lemma actpermK x a :
aperm x (
actperm a)
= to x a.
-
Lemma ker_actperm :
'ker actperm = 'C(setT | to).
+
Lemma ker_actperm :
'ker actperm = 'C(setT | to).
End ActPerm.
@@ -1268,31 +1260,31 @@
Section RestrictActionTheory.
-
Variables (
aT :
finGroupType) (
D :
{set aT}) (
rT :
finType).
+
Variables (
aT :
finGroupType) (
D :
{set aT}) (
rT :
finType).
Variables (
to :
action D rT).
-
Lemma faithful_isom (
A :
{group aT})
S (
nSA :
actby_cond A S to) :
-
[faithful A, on S | to] → isom A (
actperm <[nSA]> @* A) (
actperm <[nSA]>).
+
Lemma faithful_isom (
A :
{group aT})
S (
nSA :
actby_cond A S to) :
+
[faithful A, on S | to] → isom A (
actperm <[nSA]> @* A) (
actperm <[nSA]>).
-
Variables (
A :
{set aT}) (
sAD :
A \subset D).
+
Variables (
A :
{set aT}) (
sAD :
A \subset D).
-
Lemma ractpermE :
actperm (
to \ sAD)
=1 actperm to.
+
Lemma ractpermE :
actperm (
to \ sAD)
=1 actperm to.
-
Lemma afix_ract B :
'Fix_(to \ sAD)(B) = 'Fix_to(B).
+
Lemma afix_ract B :
'Fix_(to \ sAD)(B) = 'Fix_to(B).
-
Lemma astab_ract S :
'C(S | to \ sAD) = 'C_A(S | to).
+
Lemma astab_ract S :
'C(S | to \ sAD) = 'C_A(S | to).
-
Lemma astabs_ract S :
'N(S | to \ sAD) = 'N_A(S | to).
+
Lemma astabs_ract S :
'N(S | to \ sAD) = 'N_A(S | to).
-
Lemma acts_ract (
B :
{set aT})
S :
-
[acts B, on S | to \ sAD] = (B \subset A) && [acts B, on S | to].
+
Lemma acts_ract (
B :
{set aT})
S :
+
[acts B, on S | to \ sAD] = (B \subset A) && [acts B, on S | to].
End RestrictActionTheory.
@@ -1307,8 +1299,8 @@
-
Variables (
aT :
finGroupType) (
D :
{group aT}) (
rT :
finType).
-
Variable phi :
{morphism D >-> {perm rT}}.
+
Variables (
aT :
finGroupType) (
D :
{group aT}) (
rT :
finType).
+
Variable phi :
{morphism D >-> {perm rT}}.
Definition mact x a :=
phi a x.
@@ -1320,51 +1312,51 @@
Canonical morph_action :=
Action mact_is_action.
-
Lemma mactE x a :
morph_action x a = phi a x.
+
Lemma mactE x a :
morph_action x a = phi a x.
-
Lemma injm_faithful :
'injm phi → [faithful D, on setT | morph_action].
+
Lemma injm_faithful :
'injm phi → [faithful D, on setT | morph_action].
-
Lemma perm_mact a :
actperm morph_action a = phi a.
+
Lemma perm_mact a :
actperm morph_action a = phi a.
End MorphAct.
-
Notation "<< phi >>" := (
morph_action phi) :
action_scope.
+
Notation "<< phi >>" := (
morph_action phi) :
action_scope.
Section CompAct.
Variables (
gT aT :
finGroupType) (
rT :
finType).
-
Variables (
D :
{set aT}) (
to :
action D rT).
-
Variables (
B :
{set gT}) (
f :
{morphism B >-> aT}).
+
Variables (
D :
{set aT}) (
to :
action D rT).
+
Variables (
B :
{set gT}) (
f :
{morphism B >-> aT}).
Definition comp_act x e :=
to x (
f e).
-
Lemma comp_is_action :
is_action (
f @*^-1 D)
comp_act.
+
Lemma comp_is_action :
is_action (
f @*^-1 D)
comp_act.
Canonical comp_action :=
Action comp_is_action.
-
Lemma comp_actE x e :
comp_action x e = to x (
f e).
+
Lemma comp_actE x e :
comp_action x e = to x (
f e).
-
Lemma afix_comp (
A :
{set gT}) :
-
A \subset B → 'Fix_comp_action(A) = 'Fix_to(f @* A).
+
Lemma afix_comp (
A :
{set gT}) :
+
A \subset B → 'Fix_comp_action(A) = 'Fix_to(f @* A).
-
Lemma astab_comp S :
'C(S | comp_action) = f @*^-1 'C(S | to).
+
Lemma astab_comp S :
'C(S | comp_action) = f @*^-1 'C(S | to).
-
Lemma astabs_comp S :
'N(S | comp_action) = f @*^-1 'N(S | to).
+
Lemma astabs_comp S :
'N(S | comp_action) = f @*^-1 'N(S | to).
End CompAct.
-
Notation "to \o f" := (
comp_action to f) :
action_scope.
+
Notation "to \o f" := (
comp_action to f) :
action_scope.
Section PermAction.
@@ -1386,16 +1378,16 @@
Canonical perm_action :=
Action aperm_is_action.
-
Lemma pcycleE a :
pcycle a = orbit perm_action <[a]>%
g.
+
Lemma pcycleE a :
pcycle a = orbit perm_action <[a]>%
g.
-
Lemma perm_act1P a :
reflect (
∀ x,
aperm x a = x) (
a == 1).
+
Lemma perm_act1P a :
reflect (
∀ x,
aperm x a = x) (
a == 1).
-
Lemma perm_faithful A :
[faithful A, on setT | perm_action].
+
Lemma perm_faithful A :
[faithful A, on setT | perm_action].
-
Lemma actperm_id p :
actperm perm_action p = p.
+
Lemma actperm_id p :
actperm perm_action p = p.
End PermAction.
@@ -1403,22 +1395,22 @@
-
Notation "'P" := (
perm_action _) (
at level 8) :
action_scope.
+
Notation "'P" := (
perm_action _) (
at level 8) :
action_scope.
Section ActpermOrbits.
-
Variables (
aT :
finGroupType) (
D :
{group aT}) (
rT :
finType).
+
Variables (
aT :
finGroupType) (
D :
{group aT}) (
rT :
finType).
Variable to :
action D rT.
-
Lemma orbit_morphim_actperm (
A :
{set aT}) :
-
A \subset D → orbit 'P (
actperm to @* A)
=1 orbit to A.
+
Lemma orbit_morphim_actperm (
A :
{set aT}) :
+
A \subset D → orbit 'P (
actperm to @* A)
=1 orbit to A.
Lemma pcycle_actperm (
a :
aT) :
-
a \in D → pcycle (
actperm to a)
=1 orbit to <[a]>.
+
a \in D → pcycle (
actperm to a)
=1 orbit to <[a]>.
End ActpermOrbits.
@@ -1427,26 +1419,26 @@
Section RestrictPerm.
-
Variables (
T :
finType) (
S :
{set T}).
+
Variables (
T :
finType) (
S :
{set T}).
-
Definition restr_perm :=
actperm (
<[subxx 'N(S | 'P)]>).
-
Canonical restr_perm_morphism :=
[morphism of restr_perm].
+
Definition restr_perm :=
actperm (
<[subxx 'N(S | 'P)]>).
+
Canonical restr_perm_morphism :=
[morphism of restr_perm].
Lemma restr_perm_on p :
perm_on S (
restr_perm p).
-
Lemma triv_restr_perm p :
p \notin 'N(S | 'P) → restr_perm p = 1.
+
Lemma triv_restr_perm p :
p \notin 'N(S | 'P) → restr_perm p = 1.
-
Lemma restr_permE :
{in 'N(S | 'P) & S, ∀ p,
restr_perm p =1 p}.
+
Lemma restr_permE :
{in 'N(S | 'P) & S, ∀ p,
restr_perm p =1 p}.
-
Lemma ker_restr_perm :
'ker restr_perm = 'C(S | 'P).
+
Lemma ker_restr_perm :
'ker restr_perm = 'C(S | 'P).
-
Lemma im_restr_perm p :
restr_perm p @: S = S.
+
Lemma im_restr_perm p :
restr_perm p @: S = S.
End RestrictPerm.
@@ -1458,27 +1450,27 @@
Variable gT :
finGroupType.
-
Definition Aut_in A (
B :
{set gT}) :=
'N_A(B | 'P) / 'C_A(B | 'P).
+
Definition Aut_in A (
B :
{set gT}) :=
'N_A(B | 'P) / 'C_A(B | 'P).
-
Variables G H :
{group gT}.
-
Hypothesis sHG:
H \subset G.
+
Variables G H :
{group gT}.
+
Hypothesis sHG:
H \subset G.
-
Lemma Aut_restr_perm a :
a \in Aut G → restr_perm H a \in Aut H.
+
Lemma Aut_restr_perm a :
a \in Aut G → restr_perm H a \in Aut H.
-
Lemma restr_perm_Aut :
restr_perm H @* Aut G \subset Aut H.
+
Lemma restr_perm_Aut :
restr_perm H @* Aut G \subset Aut H.
-
Lemma Aut_in_isog :
Aut_in (
Aut G)
H \isog restr_perm H @* Aut G.
+
Lemma Aut_in_isog :
Aut_in (
Aut G)
H \isog restr_perm H @* Aut G.
Lemma Aut_sub_fullP :
-
reflect (
∀ h :
{morphism H >-> gT},
'injm h → h @* H = H →
-
∃ g :
{morphism G >-> gT},
-
[/\ 'injm g, g @* G = G & {in H, g =1 h}])
- (
Aut_in (
Aut G)
H \isog Aut H).
+
reflect (
∀ h :
{morphism H >-> gT},
'injm h → h @* H = H →
+
∃ g :
{morphism G >-> gT},
+
[/\ 'injm g, g @* G = G & {in H, g =1 h}])
+ (
Aut_in (
Aut G)
H \isog Aut H).
End AutIn.
@@ -1489,27 +1481,27 @@
Section InjmAutIn.
-
Variables (
gT rT :
finGroupType) (
D G H :
{group gT}) (
f :
{morphism D >-> rT}).
-
Hypotheses (
injf :
'injm f) (
sGD :
G \subset D) (
sHG :
H \subset G).
+
Variables (
gT rT :
finGroupType) (
D G H :
{group gT}) (
f :
{morphism D >-> rT}).
+
Hypotheses (
injf :
'injm f) (
sGD :
G \subset D) (
sHG :
H \subset G).
Let sHD :=
subset_trans sHG sGD.
Lemma astabs_Aut_isom a :
-
a \in Aut G → (fGisom a \in 'N(f @* H | 'P)) = (a \in 'N(H | 'P)).
+
a \in Aut G → (fGisom a \in 'N(f @* H | 'P)) = (a \in 'N(H | 'P)).
-
Lemma isom_restr_perm a :
a \in Aut G → fHisom (
inH a)
= infH (
fGisom a).
+
Lemma isom_restr_perm a :
a \in Aut G → fHisom (
inH a)
= infH (
fGisom a).
-
Lemma restr_perm_isom :
isom (
inH @* Aut G) (
infH @* Aut (
f @* G))
fHisom.
+
Lemma restr_perm_isom :
isom (
inH @* Aut G) (
infH @* Aut (
f @* G))
fHisom.
-
Lemma injm_Aut_sub :
Aut_in (
Aut (
f @* G)) (
f @* H)
\isog Aut_in (
Aut G)
H.
+
Lemma injm_Aut_sub :
Aut_in (
Aut (
f @* G)) (
f @* H)
\isog Aut_in (
Aut G)
H.
Lemma injm_Aut_full :
-
(Aut_in (
Aut (
f @* G)) (
f @* H)
\isog Aut (
f @* H)
)
-
= (Aut_in (
Aut G)
H \isog Aut H).
+
(Aut_in (
Aut (
f @* G)) (
f @* H)
\isog Aut (
f @* H)
)
+
= (Aut_in (
Aut G)
H \isog Aut H).
End InjmAutIn.
@@ -1518,19 +1510,19 @@
Section GroupAction.
-
Variables (
aT rT :
finGroupType) (
D :
{set aT}) (
R :
{set rT}).
+
Variables (
aT rT :
finGroupType) (
D :
{set aT}) (
R :
{set rT}).
Definition is_groupAction (
to :
actT) :=
-
{in D, ∀ a,
actperm to a \in Aut R}.
+
{in D, ∀ a,
actperm to a \in Aut R}.
Structure groupAction :=
GroupAction {
gact :>
actT;
_ :
is_groupAction gact}.
Definition clone_groupAction to :=
-
let:
GroupAction _ toA :=
to return {type of GroupAction for to} → _ in
-
fun k ⇒
k toA : groupAction.
+
let:
GroupAction _ toA :=
to return {type of GroupAction for to} → _ in
+
fun k ⇒
k toA : groupAction.
End GroupAction.
@@ -1541,7 +1533,7 @@
-
Notation "[ 'groupAction' 'of' to ]" :=
+
Notation "[ 'groupAction' 'of' to ]" :=
(
clone_groupAction (@
GroupAction _ _ _ _ to))
(
at level 0,
format "[ 'groupAction' 'of' to ]") :
form_scope.
@@ -1549,27 +1541,27 @@
Section GroupActionDefs.
-
Variables (
aT rT :
finGroupType) (
D :
{set aT}) (
R :
{set rT}).
-
Implicit Type A :
{set aT}.
-
Implicit Type S :
{set rT}.
+
Variables (
aT rT :
finGroupType) (
D :
{set aT}) (
R :
{set rT}).
+
Implicit Type A :
{set aT}.
+
Implicit Type S :
{set rT}.
Implicit Type to :
groupAction D R.
Definition gact_range of groupAction D R :=
R.
-
Definition gacent to A :=
'Fix_(R | to)(D :&: A).
+
Definition gacent to A :=
'Fix_(R | to)(D :&: A).
-
Definition acts_on_group A S to :=
[acts A, on S | to] ∧ S \subset R.
+
Definition acts_on_group A S to :=
[acts A, on S | to] ∧ S \subset R.
-
Coercion actby_cond_group A S to :
acts_on_group A S to → actby_cond A S to :=
- @
proj1 _ _.
+
Coercion actby_cond_group A S to :
acts_on_group A S to → actby_cond A S to :=
+ @
proj1 _ _.
Definition acts_irreducibly A S to :=
-
[min S of G | G :!=: 1
& [acts A, on G | to]].
+
[min S of G | G :!=: 1
& [acts A, on G | to]].
End GroupActionDefs.
@@ -1577,77 +1569,77 @@
-
Notation "''C_' ( | to ) ( A )" := (
gacent to A)
+
Notation "''C_' ( | to ) ( A )" := (
gacent to A)
(
at level 8,
format "''C_' ( | to ) ( A )") :
group_scope.
-
Notation "''C_' ( G | to ) ( A )" := (
G :&: 'C_(|to)(A))
+
Notation "''C_' ( G | to ) ( A )" := (
G :&: 'C_(|to)(A))
(
at level 8,
format "''C_' ( G | to ) ( A )") :
group_scope.
-
Notation "''C_' ( | to ) [ a ]" :=
'C_(|to)([set a])
+
Notation "''C_' ( | to ) [ a ]" :=
'C_(|to)([set a])
(
at level 8,
format "''C_' ( | to ) [ a ]") :
group_scope.
-
Notation "''C_' ( G | to ) [ a ]" :=
'C_(G | to)([set a])
+
Notation "''C_' ( G | to ) [ a ]" :=
'C_(G | to)([set a])
(
at level 8,
format "''C_' ( G | to ) [ a ]") :
group_scope.
-
Notation "{ 'acts' A , 'on' 'group' G | to }" := (
acts_on_group A G to)
+
Notation "{ 'acts' A , 'on' 'group' G | to }" := (
acts_on_group A G to)
(
at level 0,
format "{ 'acts' A , 'on' 'group' G | to }") :
form_scope.
Section RawGroupAction.
-
Variables (
aT rT :
finGroupType) (
D :
{set aT}) (
R :
{set rT}).
+
Variables (
aT rT :
finGroupType) (
D :
{set aT}) (
R :
{set rT}).
Variable to :
groupAction D R.
Lemma actperm_Aut :
is_groupAction R to.
-
Lemma im_actperm_Aut :
actperm to @* D \subset Aut R.
+
Lemma im_actperm_Aut :
actperm to @* D \subset Aut R.
-
Lemma gact_out x a :
a \in D → x \notin R → to x a = x.
+
Lemma gact_out x a :
a \in D → x \notin R → to x a = x.
-
Lemma gactM :
{in D, ∀ a,
{in R &, {morph to^~ a : x y / x × y}}}.
+
Lemma gactM :
{in D, ∀ a,
{in R &, {morph to^~ a : x y / x × y}}}.
-
Lemma actmM a :
{in R &, {morph actm to a : x y / x × y}}.
+
Lemma actmM a :
{in R &, {morph actm to a : x y / x × y}}.
Canonical act_morphism a :=
Morphism (
actmM a).
Lemma morphim_actm :
-
{in D, ∀ a (
S :
{set rT}),
S \subset R → actm to a @* S = to^* S a}.
+
{in D, ∀ a (
S :
{set rT}),
S \subset R → actm to a @* S = to^* S a}.
-
Variables (
a :
aT) (
A B :
{set aT}) (
S :
{set rT}).
+
Variables (
a :
aT) (
A B :
{set aT}) (
S :
{set rT}).
-
Lemma gacentIdom :
'C_(|to)(D :&: A) = 'C_(|to)(A).
+
Lemma gacentIdom :
'C_(|to)(D :&: A) = 'C_(|to)(A).
-
Lemma gacentIim :
'C_(R | to)(A) = 'C_(|to)(A).
+
Lemma gacentIim :
'C_(R | to)(A) = 'C_(|to)(A).
-
Lemma gacentS :
A \subset B → 'C_(|to)(B) \subset 'C_(|to)(A).
+
Lemma gacentS :
A \subset B → 'C_(|to)(B) \subset 'C_(|to)(A).
-
Lemma gacentU :
'C_(|to)(A :|: B) = 'C_(|to)(A) :&: 'C_(|to)(B).
+
Lemma gacentU :
'C_(|to)(A :|: B) = 'C_(|to)(A) :&: 'C_(|to)(B).
-
Hypotheses (
Da :
a \in D) (
sAD :
A \subset D) (
sSR :
S \subset R).
+
Hypotheses (
Da :
a \in D) (
sAD :
A \subset D) (
sSR :
S \subset R).
-
Lemma gacentE :
'C_(|to)(A) = 'Fix_(R | to)(A).
+
Lemma gacentE :
'C_(|to)(A) = 'Fix_(R | to)(A).
-
Lemma gacent1E :
'C_(|to)[a] = 'Fix_(R | to)[a].
+
Lemma gacent1E :
'C_(|to)[a] = 'Fix_(R | to)[a].
-
Lemma subgacentE :
'C_(S | to)(A) = 'Fix_(S | to)(A).
+
Lemma subgacentE :
'C_(S | to)(A) = 'Fix_(S | to)(A).
-
Lemma subgacent1E :
'C_(S | to)[a] = 'Fix_(S | to)[a].
+
Lemma subgacent1E :
'C_(S | to)[a] = 'Fix_(S | to)[a].
End RawGroupAction.
@@ -1657,130 +1649,130 @@
Variables aT rT :
finGroupType.
-
Variables (
D :
{group aT}) (
R :
{group rT}) (
to :
groupAction D R).
-
Implicit Type A B :
{set aT}.
-
Implicit Types G H :
{group aT}.
-
Implicit Type S :
{set rT}.
-
Implicit Types M N :
{group rT}.
+
Variables (
D :
{group aT}) (
R :
{group rT}) (
to :
groupAction D R).
+
Implicit Type A B :
{set aT}.
+
Implicit Types G H :
{group aT}.
+
Implicit Type S :
{set rT}.
+
Implicit Types M N :
{group rT}.
-
Lemma gact1 :
{in D, ∀ a,
to 1
a = 1
}.
+
Lemma gact1 :
{in D, ∀ a,
to 1
a = 1
}.
-
Lemma gactV :
{in D, ∀ a,
{in R, {morph to^~ a : x / x^-1}}}.
+
Lemma gactV :
{in D, ∀ a,
{in R, {morph to^~ a : x / x^-1}}}.
-
Lemma gactX :
{in D, ∀ a n,
{in R, {morph to^~ a : x / x ^+ n}}}.
+
Lemma gactX :
{in D, ∀ a n,
{in R, {morph to^~ a : x / x ^+ n}}}.
-
Lemma gactJ :
{in D, ∀ a,
{in R &, {morph to^~ a : x y / x ^ y}}}.
+
Lemma gactJ :
{in D, ∀ a,
{in R &, {morph to^~ a : x y / x ^ y}}}.
-
Lemma gactR :
{in D, ∀ a,
{in R &, {morph to^~ a : x y / [~ x, y]}}}.
+
Lemma gactR :
{in D, ∀ a,
{in R &, {morph to^~ a : x y / [~ x, y]}}}.
-
Lemma gact_stable :
{acts D, on R | to}.
+
Lemma gact_stable :
{acts D, on R | to}.
-
Lemma group_set_gacent A :
group_set 'C_(|to)(A).
+
Lemma group_set_gacent A :
group_set 'C_(|to)(A).
Canonical gacent_group A :=
Group (
group_set_gacent A).
-
Lemma gacent1 :
'C_(|to)(1
) = R.
+
Lemma gacent1 :
'C_(|to)(1
) = R.
-
Lemma gacent_gen A :
A \subset D → 'C_(|to)(<<A>>) = 'C_(|to)(A).
+
Lemma gacent_gen A :
A \subset D → 'C_(|to)(<<A>>) = 'C_(|to)(A).
-
Lemma gacentD1 A :
'C_(|to)(A^#) = 'C_(|to)(A).
+
Lemma gacentD1 A :
'C_(|to)(A^#) = 'C_(|to)(A).
-
Lemma gacent_cycle a :
a \in D → 'C_(|to)(<[a]>) = 'C_(|to)[a].
+
Lemma gacent_cycle a :
a \in D → 'C_(|to)(<[a]>) = 'C_(|to)[a].
Lemma gacentY A B :
-
A \subset D → B \subset D → 'C_(|to)(A <*> B) = 'C_(|to)(A) :&: 'C_(|to)(B).
+
A \subset D → B \subset D → 'C_(|to)(A <*> B) = 'C_(|to)(A) :&: 'C_(|to)(B).
Lemma gacentM G H :
-
G \subset D → H \subset D → 'C_(|to)(G × H) = 'C_(|to)(G) :&: 'C_(|to)(H).
+
G \subset D → H \subset D → 'C_(|to)(G × H) = 'C_(|to)(G) :&: 'C_(|to)(H).
-
Lemma astab1 :
'C(1
| to) = D.
+
Lemma astab1 :
'C(1
| to) = D.
-
Lemma astab_range :
'C(R | to) = 'C(setT | to).
+
Lemma astab_range :
'C(R | to) = 'C(setT | to).
Lemma gacentC A S :
-
A \subset D → S \subset R →
-
(S \subset 'C_(|to)(A)) = (A \subset 'C(S | to)).
+
A \subset D → S \subset R →
+
(S \subset 'C_(|to)(A)) = (A \subset 'C(S | to)).
-
Lemma astab_gen S :
S \subset R → 'C(<<S>> | to) = 'C(S | to).
+
Lemma astab_gen S :
S \subset R → 'C(<<S>> | to) = 'C(S | to).
Lemma astabM M N :
-
M \subset R → N \subset R → 'C(M × N | to) = 'C(M | to) :&: 'C(N | to).
+
M \subset R → N \subset R → 'C(M × N | to) = 'C(M | to) :&: 'C(N | to).
-
Lemma astabs1 :
'N(1
| to) = D.
+
Lemma astabs1 :
'N(1
| to) = D.
-
Lemma astabs_range :
'N(R | to) = D.
+
Lemma astabs_range :
'N(R | to) = D.
-
Lemma astabsD1 S :
'N(S^# | to) = 'N(S | to).
+
Lemma astabsD1 S :
'N(S^# | to) = 'N(S | to).
-
Lemma gacts_range A :
A \subset D → {acts A, on group R | to}.
+
Lemma gacts_range A :
A \subset D → {acts A, on group R | to}.
-
Lemma acts_subnorm_gacent A :
A \subset D →
-
[acts 'N_D(A), on 'C_(| to)(A) | to].
+
Lemma acts_subnorm_gacent A :
A \subset D →
+
[acts 'N_D(A), on 'C_(| to)(A) | to].
Lemma acts_subnorm_subgacent A B S :
-
A \subset D → [acts B, on S | to] → [acts 'N_B(A), on 'C_(S | to)(A) | to].
+
A \subset D → [acts B, on S | to] → [acts 'N_B(A), on 'C_(S | to)(A) | to].
Lemma acts_gen A S :
-
S \subset R → [acts A, on S | to] → [acts A, on <<S>> | to].
+
S \subset R → [acts A, on S | to] → [acts A, on <<S>> | to].
Lemma acts_joing A M N :
-
M \subset R → N \subset R → [acts A, on M | to] → [acts A, on N | to] →
-
[acts A, on M <*> N | to].
+
M \subset R → N \subset R → [acts A, on M | to] → [acts A, on N | to] →
+
[acts A, on M <*> N | to].
-
Lemma injm_actm a :
'injm (actm to a).
+
Lemma injm_actm a :
'injm (actm to a).
-
Lemma im_actm a :
actm to a @* R = R.
+
Lemma im_actm a :
actm to a @* R = R.
-
Lemma acts_char G M :
G \subset D → M \char R → [acts G, on M | to].
+
Lemma acts_char G M :
G \subset D → M \char R → [acts G, on M | to].
Lemma gacts_char G M :
-
G \subset D → M \char R → {acts G, on group M | to}.
+
G \subset D → M \char R → {acts G, on group M | to}.
Section Restrict.
-
Variables (
A :
{group aT}) (
sAD :
A \subset D).
+
Variables (
A :
{group aT}) (
sAD :
A \subset D).
-
Lemma ract_is_groupAction :
is_groupAction R (
to \ sAD).
+
Lemma ract_is_groupAction :
is_groupAction R (
to \ sAD).
Canonical ract_groupAction :=
GroupAction ract_is_groupAction.
-
Lemma gacent_ract B :
'C_(|ract_groupAction)(B) = 'C_(|to)(A :&: B).
+
Lemma gacent_ract B :
'C_(|ract_groupAction)(B) = 'C_(|to)(A :&: B).
End Restrict.
@@ -1789,17 +1781,17 @@
Section ActBy.
-
Variables (
A :
{group aT}) (
G :
{group rT}) (
nGAg :
{acts A, on group G | to}).
+
Variables (
A :
{group aT}) (
G :
{group rT}) (
nGAg :
{acts A, on group G | to}).
-
Lemma actby_is_groupAction :
is_groupAction G <[nGAg]>.
+
Lemma actby_is_groupAction :
is_groupAction G <[nGAg]>.
Canonical actby_groupAction :=
GroupAction actby_is_groupAction.
Lemma gacent_actby B :
-
'C_(|actby_groupAction)(B) = 'C_(G | to)(A :&: B).
+
'C_(|actby_groupAction)(B) = 'C_(G | to)(A :&: B).
End ActBy.
@@ -1808,19 +1800,19 @@
Section Quotient.
-
Variable H :
{group rT}.
+
Variable H :
{group rT}.
-
Lemma acts_qact_dom_norm :
{acts qact_dom to H, on 'N(H) | to}.
+
Lemma acts_qact_dom_norm :
{acts qact_dom to H, on 'N(H) | to}.
-
Lemma qact_is_groupAction :
is_groupAction (
R / H) (
to / H).
+
Lemma qact_is_groupAction :
is_groupAction (
R / H) (
to / H).
Canonical quotient_groupAction :=
GroupAction qact_is_groupAction.
-
Lemma qact_domE :
H \subset R → qact_dom to H = 'N(H | to).
+
Lemma qact_domE :
H \subset R → qact_dom to H = 'N(H | to).
End Quotient.
@@ -1829,52 +1821,52 @@
Section Mod.
-
Variable H :
{group aT}.
+
Variable H :
{group aT}.
-
Lemma modact_is_groupAction :
is_groupAction 'C_(|to)(H) (
to %% H).
+
Lemma modact_is_groupAction :
is_groupAction 'C_(|to)(H) (
to %% H).
Canonical mod_groupAction :=
GroupAction modact_is_groupAction.
Lemma modgactE x a :
-
H \subset 'C(R | to) → a \in 'N_D(H) → (
to %% H)%
act x (
coset H a)
= to x a.
+
H \subset 'C(R | to) → a \in 'N_D(H) → (
to %% H)%
act x (
coset H a)
= to x a.
Lemma gacent_mod G M :
-
H \subset 'C(M | to) → G \subset 'N(H) →
-
'C_(M | mod_groupAction)(G / H) = 'C_(M | to)(G).
+
H \subset 'C(M | to) → G \subset 'N(H) →
+
'C_(M | mod_groupAction)(G / H) = 'C_(M | to)(G).
Lemma acts_irr_mod G M :
-
H \subset 'C(M | to) → G \subset 'N(H) → acts_irreducibly G M to →
-
acts_irreducibly (
G / H)
M mod_groupAction.
+
H \subset 'C(M | to) → G \subset 'N(H) → acts_irreducibly G M to →
+
acts_irreducibly (
G / H)
M mod_groupAction.
End Mod.
Lemma modact_coset_astab x a :
-
a \in D → (
to %% 'C(R | to))%
act x (
coset _ a)
= to x a.
+
a \in D → (
to %% 'C(R | to))%
act x (
coset _ a)
= to x a.
Lemma acts_irr_mod_astab G M :
-
acts_irreducibly G M to →
-
acts_irreducibly (
G / 'C_G(M | to))
M (
mod_groupAction _).
+
acts_irreducibly G M to →
+
acts_irreducibly (
G / 'C_G(M | to))
M (
mod_groupAction _).
Section CompAct.
-
Variables (
gT :
finGroupType) (
G :
{group gT}) (
f :
{morphism G >-> aT}).
+
Variables (
gT :
finGroupType) (
G :
{group gT}) (
f :
{morphism G >-> aT}).
Lemma comp_is_groupAction :
is_groupAction R (
comp_action to f).
Canonical comp_groupAction :=
GroupAction comp_is_groupAction.
-
Lemma gacent_comp U :
'C_(|comp_groupAction)(U) = 'C_(|to)(f @* U).
+
Lemma gacent_comp U :
'C_(|comp_groupAction)(U) = 'C_(|to)(f @* U).
End CompAct.
@@ -1883,19 +1875,19 @@
End GroupActionTheory.
-
Notation "''C_' ( | to ) ( A )" := (
gacent_group to A) :
Group_scope.
-
Notation "''C_' ( G | to ) ( A )" :=
- (
setI_group G 'C_(|to)(A)) :
Group_scope.
-
Notation "''C_' ( | to ) [ a ]" := (
gacent_group to [set a%
g]) :
Group_scope.
-
Notation "''C_' ( G | to ) [ a ]" :=
- (
setI_group G 'C_(|to)[a]) :
Group_scope.
+
Notation "''C_' ( | to ) ( A )" := (
gacent_group to A) :
Group_scope.
+
Notation "''C_' ( G | to ) ( A )" :=
+ (
setI_group G 'C_(|to)(A)) :
Group_scope.
+
Notation "''C_' ( | to ) [ a ]" := (
gacent_group to [set a%
g]) :
Group_scope.
+
Notation "''C_' ( G | to ) [ a ]" :=
+ (
setI_group G 'C_(|to)[a]) :
Group_scope.
-
Notation "to \ sAD" := (
ract_groupAction to sAD) :
groupAction_scope.
-
Notation "<[ nGA ] >" := (
actby_groupAction nGA) :
groupAction_scope.
-
Notation "to / H" := (
quotient_groupAction to H) :
groupAction_scope.
-
Notation "to %% H" := (
mod_groupAction to H) :
groupAction_scope.
-
Notation "to \o f" := (
comp_groupAction to f) :
groupAction_scope.
+
Notation "to \ sAD" := (
ract_groupAction to sAD) :
groupAction_scope.
+
Notation "<[ nGA ] >" := (
actby_groupAction nGA) :
groupAction_scope.
+
Notation "to / H" := (
quotient_groupAction to H) :
groupAction_scope.
+
Notation "to %% H" := (
mod_groupAction to H) :
groupAction_scope.
+
Notation "to \o f" := (
comp_groupAction to f) :
groupAction_scope.
@@ -1908,23 +1900,23 @@
Variables (
aT1 aT2 :
finGroupType) (
rT1 rT2 :
finType).
-
Variables (
D1 :
{group aT1}) (
D2 :
{group aT2}).
+
Variables (
D1 :
{group aT1}) (
D2 :
{group aT2}).
Variables (
to1 :
action D1 rT1) (
to2 :
action D2 rT2).
-
Variables (
A :
{set aT1}) (
R S :
{set rT1}).
-
Variables (
h :
rT1 → rT2) (
f :
{morphism D1 >-> aT2}).
-
Hypotheses (
actsDR :
{acts D1, on R | to1}) (
injh :
{in R &, injective h}).
-
Hypothesis defD2 :
f @* D1 = D2.
-
Hypotheses (
sSR :
S \subset R) (
sAD1 :
A \subset D1).
-
Hypothesis hfJ :
{in S & D1, morph_act to1 to2 h f}.
+
Variables (
A :
{set aT1}) (
R S :
{set rT1}).
+
Variables (
h :
rT1 → rT2) (
f :
{morphism D1 >-> aT2}).
+
Hypotheses (
actsDR :
{acts D1, on R | to1}) (
injh :
{in R &, injective h}).
+
Hypothesis defD2 :
f @* D1 = D2.
+
Hypotheses (
sSR :
S \subset R) (
sAD1 :
A \subset D1).
+
Hypothesis hfJ :
{in S & D1, morph_act to1 to2 h f}.
-
Lemma morph_astabs :
f @* 'N(S | to1) = 'N(h @: S | to2).
+
Lemma morph_astabs :
f @* 'N(S | to1) = 'N(h @: S | to2).
-
Lemma morph_astab :
f @* 'C(S | to1) = 'C(h @: S | to2).
+
Lemma morph_astab :
f @* 'C(S | to1) = 'C(h @: S | to2).
-
Lemma morph_afix :
h @: 'Fix_(S | to1)(A) = 'Fix_(h @: S | to2)(f @* A).
+
Lemma morph_afix :
h @: 'Fix_(S | to1)(A) = 'Fix_(h @: S | to2)(f @* A).
End MorphAction.
@@ -1934,27 +1926,27 @@
Variables (
aT1 aT2 rT1 rT2 :
finGroupType).
-
Variables (
D1 :
{group aT1}) (
D2 :
{group aT2}).
-
Variables (
R1 :
{group rT1}) (
R2 :
{group rT2}).
+
Variables (
D1 :
{group aT1}) (
D2 :
{group aT2}).
+
Variables (
R1 :
{group rT1}) (
R2 :
{group rT2}).
Variables (
to1 :
groupAction D1 R1) (
to2 :
groupAction D2 R2).
-
Variables (
h :
{morphism R1 >-> rT2}) (
f :
{morphism D1 >-> aT2}).
+
Variables (
h :
{morphism R1 >-> rT2}) (
f :
{morphism D1 >-> aT2}).
Hypotheses (
iso_h :
isom R1 R2 h) (
iso_f :
isom D1 D2 f).
-
Hypothesis hfJ :
{in R1 & D1, morph_act to1 to2 h f}.
-
Implicit Types (
A :
{set aT1}) (
S :
{set rT1}) (
M :
{group rT1}).
+
Hypothesis hfJ :
{in R1 & D1, morph_act to1 to2 h f}.
+
Implicit Types (
A :
{set aT1}) (
S :
{set rT1}) (
M :
{group rT1}).
-
Lemma morph_gastabs S :
S \subset R1 → f @* 'N(S | to1) = 'N(h @* S | to2).
+
Lemma morph_gastabs S :
S \subset R1 → f @* 'N(S | to1) = 'N(h @* S | to2).
-
Lemma morph_gastab S :
S \subset R1 → f @* 'C(S | to1) = 'C(h @* S | to2).
+
Lemma morph_gastab S :
S \subset R1 → f @* 'C(S | to1) = 'C(h @* S | to2).
-
Lemma morph_gacent A :
A \subset D1 → h @* 'C_(|to1)(A) = 'C_(|to2)(f @* A).
+
Lemma morph_gacent A :
A \subset D1 → h @* 'C_(|to1)(A) = 'C_(|to2)(f @* A).
Lemma morph_gact_irr A M :
-
A \subset D1 → M \subset R1 →
-
acts_irreducibly (
f @* A) (
h @* M)
to2 = acts_irreducibly A M to1.
+
A \subset D1 → M \subset R1 →
+
acts_irreducibly (
f @* A) (
h @* M)
to2 = acts_irreducibly A M to1.
End MorphGroupAction.
@@ -1970,8 +1962,8 @@
Variable gT :
finGroupType.
-
Implicit Type A :
{set gT}.
-
Implicit Type G :
{group gT}.
+
Implicit Type A :
{set gT}.
+
Implicit Type G :
{group gT}.
@@ -2012,22 +2004,22 @@