From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 22 May 2019 13:43:08 +0200
Subject: htmldoc regenerated
---
docs/htmldoc/mathcomp.fingroup.fingroup.html | 1631 +++++++++++++-------------
1 file changed, 801 insertions(+), 830 deletions(-)
(limited to 'docs/htmldoc/mathcomp.fingroup.fingroup.html')
diff --git a/docs/htmldoc/mathcomp.fingroup.fingroup.html b/docs/htmldoc/mathcomp.fingroup.fingroup.html
index c406f39..fcade98 100644
--- a/docs/htmldoc/mathcomp.fingroup.fingroup.html
+++ b/docs/htmldoc/mathcomp.fingroup.fingroup.html
@@ -21,7 +21,6 @@
@@ -248,13 +247,13 @@
Record mixin_of (
T :
Type) :
Type :=
BaseMixin {
-
mul :
T → T → T;
+
mul :
T → T → T;
one :
T;
-
inv :
T → T;
-
_ :
associative mul;
-
_ :
left_id one mul;
-
_ :
involutive inv;
-
_ :
{morph inv : x y / mul x y >-> mul y x}
+
inv :
T → T;
+
_ :
associative mul;
+
_ :
left_id one mul;
+
_ :
involutive inv;
+
_ :
{morph inv : x y / mul x y >-> mul y x}
}.
@@ -301,7 +300,7 @@
Structure type :
Type :=
Pack {
base :
base_type;
-
_ :
left_inverse (
one (
mixin base)) (
inv (
mixin base)) (
mul (
mixin base))
+
_ :
left_inverse (
one (
mixin base)) (
inv (
mixin base)) (
mul (
mixin base))
}.
@@ -316,21 +315,21 @@
Section Mixin.
-
Variables (
T :
Type) (
one :
T) (
mul :
T → T → T) (
inv :
T → T).
+
Variables (
T :
Type) (
one :
T) (
mul :
T → T → T) (
inv :
T → T).
-
Hypothesis mulA :
associative mul.
-
Hypothesis mul1 :
left_id one mul.
-
Hypothesis mulV :
left_inverse one inv mul.
-
Notation "1" :=
one.
-
Infix "×" :=
mul.
-
Notation "x ^-1" := (
inv x).
+
Hypothesis mulA :
associative mul.
+
Hypothesis mul1 :
left_id one mul.
+
Hypothesis mulV :
left_inverse one inv mul.
+
Notation "1" :=
one.
+
Infix "×" :=
mul.
+
Notation "x ^-1" := (
inv x).
-
Lemma mk_invgK :
involutive inv.
+
Lemma mk_invgK :
involutive inv.
-
Lemma mk_invMg :
{morph inv : x y / x × y >-> y × x}.
+
Lemma mk_invMg :
{morph inv : x y / x × y >-> y × x}.
Definition Mixin :=
BaseMixin mulA mul1 mk_invgK mk_invMg.
@@ -340,17 +339,17 @@
Definition pack_base T m :=
-
fun c cT &
phant_id (
Finite.class cT)
c ⇒ @
PackBase T m c.
+
fun c cT &
phant_id (
Finite.class cT)
c ⇒ @
PackBase T m c.
Definition clone_base T :=
-
fun bT &
sort bT → T ⇒
-
fun m c (
bT' := @
PackBase T m c) &
phant_id bT' bT ⇒
bT'.
+
fun bT &
sort bT → T ⇒
+
fun m c (
bT' := @
PackBase T m c) &
phant_id bT' bT ⇒
bT'.
Definition clone T :=
-
fun bT gT &
sort bT × sort (
base gT)
→ T × T ⇒
-
fun m (
gT' := @
Pack bT m) &
phant_id gT' gT ⇒
gT'.
+
fun bT gT &
sort bT × sort (
base gT)
→ T × T ⇒
+
fun m (
gT' := @
Pack bT m) &
phant_id gT' gT ⇒
gT'.
Section InheritedClasses.
@@ -359,14 +358,14 @@
Variable bT :
base_type.
-
Canonical eqType :=
Equality.Pack class rT.
-
Canonical choiceType :=
Choice.Pack class rT.
-
Canonical countType :=
Countable.Pack class rT.
-
Canonical finType :=
Finite.Pack class rT.
-
Definition arg_eqType :=
Eval hnf in [eqType of T].
-
Definition arg_choiceType :=
Eval hnf in [choiceType of T].
-
Definition arg_countType :=
Eval hnf in [countType of T].
-
Definition arg_finType :=
Eval hnf in [finType of T].
+
Canonical eqType :=
Equality.Pack class.
+
Canonical choiceType :=
Choice.Pack class.
+
Canonical countType :=
Countable.Pack class.
+
Canonical finType :=
Finite.Pack class.
+
Definition arg_eqType :=
Eval hnf in [eqType of T].
+
Definition arg_choiceType :=
Eval hnf in [choiceType of T].
+
Definition arg_countType :=
Eval hnf in [countType of T].
+
Definition arg_finType :=
Eval hnf in [finType of T].
End InheritedClasses.
@@ -400,11 +399,11 @@
Canonical arg_finType.
Notation baseFinGroupType :=
base_type.
Notation finGroupType :=
type.
-
Notation BaseFinGroupType T m := (@
pack_base T m _ _ id).
+
Notation BaseFinGroupType T m := (@
pack_base T m _ _ id).
Notation FinGroupType :=
Pack.
-
Notation "[ 'baseFinGroupType' 'of' T ]" := (@
clone_base T _ id _ _ id)
+
Notation "[ 'baseFinGroupType' 'of' T ]" := (@
clone_base T _ id _ _ id)
(
at level 0,
format "[ 'baseFinGroupType' 'of' T ]") :
form_scope.
-
Notation "[ 'finGroupType' 'of' T ]" := (@
clone T _ _ id _ id)
+
Notation "[ 'finGroupType' 'of' T ]" := (@
clone T _ _ id _ id)
(
at level 0,
format "[ 'finGroupType' 'of' T ]") :
form_scope.
End Exports.
@@ -421,22 +420,22 @@
Definition oneg :
rT :=
FinGroup.one T.
-
Definition mulg :
T → T → rT :=
FinGroup.mul T.
-
Definition invg :
T → rT :=
FinGroup.inv T.
+
Definition mulg :
T → T → rT :=
FinGroup.mul T.
+
Definition invg :
T → rT :=
FinGroup.inv T.
Definition expgn_rec (
x :
T)
n :
rT :=
iterop n mulg x oneg.
End ElementOps.
-
Definition expgn :=
nosimpl expgn_rec.
+
Definition expgn :=
nosimpl expgn_rec.
-
Notation "1" := (
oneg _) :
group_scope.
-
Notation "x1 * x2" := (
mulg x1 x2) :
group_scope.
-
Notation "x ^-1" := (
invg x) :
group_scope.
-
Notation "x ^+ n" := (
expgn x n) :
group_scope.
-
Notation "x ^- n" :=
(x ^+ n)^-1 :
group_scope.
+
Notation "1" := (
oneg _) :
group_scope.
+
Notation "x1 * x2" := (
mulg x1 x2) :
group_scope.
+
Notation "x ^-1" := (
invg x) :
group_scope.
+
Notation "x ^+ n" := (
expgn x n) :
group_scope.
+
Notation "x ^- n" :=
(x ^+ n)^-1 :
group_scope.
@@ -447,41 +446,41 @@
{x^-1 * (y * z) | y \in A, x, z \in B}
-
Definition conjg (
T :
finGroupType) (
x y :
T) :=
y^-1 × (x × y).
-
Notation "x1 ^ x2" := (
conjg x1 x2) :
group_scope.
+
Definition conjg (
T :
finGroupType) (
x y :
T) :=
y^-1 × (x × y).
+
Notation "x1 ^ x2" := (
conjg x1 x2) :
group_scope.
-
Definition commg (
T :
finGroupType) (
x y :
T) :=
x^-1 × x ^ y.
-
Notation "[ ~ x1 , x2 , .. , xn ]" := (
commg .. (
commg x1 x2) ..
xn)
+
Definition commg (
T :
finGroupType) (
x y :
T) :=
x^-1 × x ^ y.
+
Notation "[ ~ x1 , x2 , .. , xn ]" := (
commg .. (
commg x1 x2) ..
xn)
:
group_scope.
-
Notation "\prod_ ( i <- r | P ) F" :=
- (
\big[mulg/1
]_(i <- r | P%
B) F%
g) :
group_scope.
-
Notation "\prod_ ( i <- r ) F" :=
- (
\big[mulg/1
]_(i <- r) F%
g) :
group_scope.
-
Notation "\prod_ ( m <= i < n | P ) F" :=
- (
\big[mulg/1
]_(m ≤ i < n | P%
B) F%
g) :
group_scope.
-
Notation "\prod_ ( m <= i < n ) F" :=
- (
\big[mulg/1
]_(m ≤ i < n) F%
g) :
group_scope.
-
Notation "\prod_ ( i | P ) F" :=
- (
\big[mulg/1
]_(i | P%
B) F%
g) :
group_scope.
-
Notation "\prod_ i F" :=
- (
\big[mulg/1
]_i F%
g) :
group_scope.
-
Notation "\prod_ ( i : t | P ) F" :=
- (
\big[mulg/1
]_(i : t | P%
B) F%
g) (
only parsing) :
group_scope.
-
Notation "\prod_ ( i : t ) F" :=
- (
\big[mulg/1
]_(i : t) F%
g) (
only parsing) :
group_scope.
-
Notation "\prod_ ( i < n | P ) F" :=
- (
\big[mulg/1
]_(i < n | P%
B) F%
g) :
group_scope.
-
Notation "\prod_ ( i < n ) F" :=
- (
\big[mulg/1
]_(i < n) F%
g) :
group_scope.
-
Notation "\prod_ ( i 'in' A | P ) F" :=
- (
\big[mulg/1
]_(i in A | P%
B) F%
g) :
group_scope.
-
Notation "\prod_ ( i 'in' A ) F" :=
- (
\big[mulg/1
]_(i in A) F%
g) :
group_scope.
+
Notation "\prod_ ( i <- r | P ) F" :=
+ (
\big[mulg/1
]_(i <- r | P%
B) F%
g) :
group_scope.
+
Notation "\prod_ ( i <- r ) F" :=
+ (
\big[mulg/1
]_(i <- r) F%
g) :
group_scope.
+
Notation "\prod_ ( m <= i < n | P ) F" :=
+ (
\big[mulg/1
]_(m ≤ i < n | P%
B) F%
g) :
group_scope.
+
Notation "\prod_ ( m <= i < n ) F" :=
+ (
\big[mulg/1
]_(m ≤ i < n) F%
g) :
group_scope.
+
Notation "\prod_ ( i | P ) F" :=
+ (
\big[mulg/1
]_(i | P%
B) F%
g) :
group_scope.
+
Notation "\prod_ i F" :=
+ (
\big[mulg/1
]_i F%
g) :
group_scope.
+
Notation "\prod_ ( i : t | P ) F" :=
+ (
\big[mulg/1
]_(i : t | P%
B) F%
g) (
only parsing) :
group_scope.
+
Notation "\prod_ ( i : t ) F" :=
+ (
\big[mulg/1
]_(i : t) F%
g) (
only parsing) :
group_scope.
+
Notation "\prod_ ( i < n | P ) F" :=
+ (
\big[mulg/1
]_(i < n | P%
B) F%
g) :
group_scope.
+
Notation "\prod_ ( i < n ) F" :=
+ (
\big[mulg/1
]_(i < n) F%
g) :
group_scope.
+
Notation "\prod_ ( i 'in' A | P ) F" :=
+ (
\big[mulg/1
]_(i in A | P%
B) F%
g) :
group_scope.
+
Notation "\prod_ ( i 'in' A ) F" :=
+ (
\big[mulg/1
]_(i in A) F%
g) :
group_scope.
Section PreGroupIdentities.
@@ -491,86 +490,86 @@
Implicit Types x y z :
T.
-
Lemma mulgA :
associative mulgT.
-
Lemma mul1g :
left_id 1
mulgT.
-
Lemma invgK : @
involutive T invg.
-
Lemma invMg x y :
(x × y)^-1 = y^-1 × x^-1.
+
Lemma mulgA :
associative mulgT.
+
Lemma mul1g :
left_id 1
mulgT.
+
Lemma invgK : @
involutive T invg.
+
Lemma invMg x y :
(x × y)^-1 = y^-1 × x^-1.
-
Lemma invg_inj : @
injective T T invg.
+
Lemma invg_inj : @
injective T T invg.
-
Lemma eq_invg_sym x y :
(x^-1 == y) = (x == y^-1).
+
Lemma eq_invg_sym x y :
(x^-1 == y) = (x == y^-1).
-
Lemma invg1 : 1
^-1 = 1
:> T.
+
Lemma invg1 : 1
^-1 = 1
:> T.
-
Lemma eq_invg1 x :
(x^-1 == 1
) = (x == 1
).
+
Lemma eq_invg1 x :
(x^-1 == 1
) = (x == 1
).
-
Lemma mulg1 :
right_id 1
mulgT.
+
Lemma mulg1 :
right_id 1
mulgT.
Canonical finGroup_law :=
Monoid.Law mulgA mul1g mulg1.
-
Lemma expgnE x n :
x ^+ n = expgn_rec x n.
+
Lemma expgnE x n :
x ^+ n = expgn_rec x n.
-
Lemma expg0 x :
x ^+ 0
= 1.
-
Lemma expg1 x :
x ^+ 1
= x.
+
Lemma expg0 x :
x ^+ 0
= 1.
+
Lemma expg1 x :
x ^+ 1
= x.
-
Lemma expgS x n :
x ^+ n.+1 = x × x ^+ n.
+
Lemma expgS x n :
x ^+ n.+1 = x × x ^+ n.
-
Lemma expg1n n : 1
^+ n = 1
:> T.
+
Lemma expg1n n : 1
^+ n = 1
:> T.
-
Lemma expgD x n m :
x ^+ (n + m) = x ^+ n × x ^+ m.
+
Lemma expgD x n m :
x ^+ (n + m) = x ^+ n × x ^+ m.
-
Lemma expgSr x n :
x ^+ n.+1 = x ^+ n × x.
+
Lemma expgSr x n :
x ^+ n.+1 = x ^+ n × x.
-
Lemma expgM x n m :
x ^+ (n × m) = x ^+ n ^+ m.
+
Lemma expgM x n m :
x ^+ (n × m) = x ^+ n ^+ m.
-
Lemma expgAC x m n :
x ^+ m ^+ n = x ^+ n ^+ m.
+
Lemma expgAC x m n :
x ^+ m ^+ n = x ^+ n ^+ m.
-
Definition commute x y :=
x × y = y × x.
+
Definition commute x y :=
x × y = y × x.
Lemma commute_refl x :
commute x x.
-
Lemma commute_sym x y :
commute x y → commute y x.
+
Lemma commute_sym x y :
commute x y → commute y x.
Lemma commute1 x :
commute x 1.
-
Lemma commuteM x y z :
commute x y → commute x z → commute x (
y × z).
+
Lemma commuteM x y z :
commute x y → commute x z → commute x (
y × z).
-
Lemma commuteX x y n :
commute x y → commute x (
y ^+ n).
+
Lemma commuteX x y n :
commute x y → commute x (
y ^+ n).
-
Lemma commuteX2 x y m n :
commute x y → commute (
x ^+ m) (
y ^+ n).
+
Lemma commuteX2 x y m n :
commute x y → commute (
x ^+ m) (
y ^+ n).
-
Lemma expgVn x n :
x^-1 ^+ n = x ^- n.
+
Lemma expgVn x n :
x^-1 ^+ n = x ^- n.
-
Lemma expgMn x y n :
commute x y → (x × y) ^+ n = x ^+ n × y ^+ n.
+
Lemma expgMn x y n :
commute x y → (x × y) ^+ n = x ^+ n × y ^+ n.
End PreGroupIdentities.
-
Hint Resolve commute1.
+
Hint Resolve commute1 :
core.
Section GroupIdentities.
@@ -580,131 +579,131 @@
Implicit Types x y z :
T.
-
Lemma mulVg :
left_inverse 1
invg mulgT.
+
Lemma mulVg :
left_inverse 1
invg mulgT.
-
Lemma mulgV :
right_inverse 1
invg mulgT.
+
Lemma mulgV :
right_inverse 1
invg mulgT.
-
Lemma mulKg :
left_loop invg mulgT.
+
Lemma mulKg :
left_loop invg mulgT.
-
Lemma mulKVg :
rev_left_loop invg mulgT.
+
Lemma mulKVg :
rev_left_loop invg mulgT.
-
Lemma mulgI :
right_injective mulgT.
+
Lemma mulgI :
right_injective mulgT.
-
Lemma mulgK :
right_loop invg mulgT.
+
Lemma mulgK :
right_loop invg mulgT.
-
Lemma mulgKV :
rev_right_loop invg mulgT.
+
Lemma mulgKV :
rev_right_loop invg mulgT.
-
Lemma mulIg :
left_injective mulgT.
+
Lemma mulIg :
left_injective mulgT.
-
Lemma eq_invg_mul x y :
(x^-1 == y :> T) = (x × y == 1
:> T).
+
Lemma eq_invg_mul x y :
(x^-1 == y :> T) = (x × y == 1
:> T).
-
Lemma eq_mulgV1 x y :
(x == y) = (x × y^-1 == 1
:> T).
+
Lemma eq_mulgV1 x y :
(x == y) = (x × y^-1 == 1
:> T).
-
Lemma eq_mulVg1 x y :
(x == y) = (x^-1 × y == 1
:> T).
+
Lemma eq_mulVg1 x y :
(x == y) = (x^-1 × y == 1
:> T).
-
Lemma commuteV x y :
commute x y → commute x y^-1.
+
Lemma commuteV x y :
commute x y → commute x y^-1.
-
Lemma conjgE x y :
x ^ y = y^-1 × (x × y).
+
Lemma conjgE x y :
x ^ y = y^-1 × (x × y).
-
Lemma conjgC x y :
x × y = y × x ^ y.
+
Lemma conjgC x y :
x × y = y × x ^ y.
-
Lemma conjgCV x y :
x × y = y ^ x^-1 × x.
+
Lemma conjgCV x y :
x × y = y ^ x^-1 × x.
-
Lemma conjg1 x :
x ^ 1
= x.
+
Lemma conjg1 x :
x ^ 1
= x.
-
Lemma conj1g x : 1
^ x = 1.
+
Lemma conj1g x : 1
^ x = 1.
-
Lemma conjMg x y z :
(x × y) ^ z = x ^ z × y ^ z.
+
Lemma conjMg x y z :
(x × y) ^ z = x ^ z × y ^ z.
-
Lemma conjgM x y z :
x ^ (y × z) = (x ^ y) ^ z.
+
Lemma conjgM x y z :
x ^ (y × z) = (x ^ y) ^ z.
-
Lemma conjVg x y :
x^-1 ^ y = (x ^ y)^-1.
+
Lemma conjVg x y :
x^-1 ^ y = (x ^ y)^-1.
-
Lemma conjJg x y z :
(x ^ y) ^ z = (x ^ z) ^ y ^ z.
+
Lemma conjJg x y z :
(x ^ y) ^ z = (x ^ z) ^ y ^ z.
-
Lemma conjXg x y n :
(x ^+ n) ^ y = (x ^ y) ^+ n.
+
Lemma conjXg x y n :
(x ^+ n) ^ y = (x ^ y) ^+ n.
-
Lemma conjgK : @
right_loop T T invg conjg.
+
Lemma conjgK : @
right_loop T T invg conjg.
-
Lemma conjgKV : @
rev_right_loop T T invg conjg.
+
Lemma conjgKV : @
rev_right_loop T T invg conjg.
-
Lemma conjg_inj : @
left_injective T T T conjg.
+
Lemma conjg_inj : @
left_injective T T T conjg.
-
Lemma conjg_eq1 x y :
(x ^ y == 1
) = (x == 1
).
+
Lemma conjg_eq1 x y :
(x ^ y == 1
) = (x == 1
).
-
Lemma conjg_prod I r (
P :
pred I)
F z :
-
(\prod_(i <- r | P i) F i) ^ z = \prod_(i <- r | P i) (F i ^ z).
+
Lemma conjg_prod I r (
P :
pred I)
F z :
+
(\prod_(i <- r | P i) F i) ^ z = \prod_(i <- r | P i) (F i ^ z).
-
Lemma commgEl x y :
[~ x, y] = x^-1 × x ^ y.
+
Lemma commgEl x y :
[~ x, y] = x^-1 × x ^ y.
-
Lemma commgEr x y :
[~ x, y] = y^-1 ^ x × y.
+
Lemma commgEr x y :
[~ x, y] = y^-1 ^ x × y.
-
Lemma commgC x y :
x × y = y × x × [~ x, y].
+
Lemma commgC x y :
x × y = y × x × [~ x, y].
-
Lemma commgCV x y :
x × y = [~ x^-1, y^-1] × (y × x).
+
Lemma commgCV x y :
x × y = [~ x^-1, y^-1] × (y × x).
-
Lemma conjRg x y z :
[~ x, y] ^ z = [~ x ^ z, y ^ z].
+
Lemma conjRg x y z :
[~ x, y] ^ z = [~ x ^ z, y ^ z].
-
Lemma invg_comm x y :
[~ x, y]^-1 = [~ y, x].
+
Lemma invg_comm x y :
[~ x, y]^-1 = [~ y, x].
-
Lemma commgP x y :
reflect (
commute x y) (
[~ x, y] == 1
:> T).
+
Lemma commgP x y :
reflect (
commute x y) (
[~ x, y] == 1
:> T).
-
Lemma conjg_fixP x y :
reflect (
x ^ y = x) (
[~ x, y] == 1
:> T).
+
Lemma conjg_fixP x y :
reflect (
x ^ y = x) (
[~ x, y] == 1
:> T).
-
Lemma commg1_sym x y :
([~ x, y] == 1
:> T) = ([~ y, x] == 1
:> T).
+
Lemma commg1_sym x y :
([~ x, y] == 1
:> T) = ([~ y, x] == 1
:> T).
-
Lemma commg1 x :
[~ x, 1
] = 1.
+
Lemma commg1 x :
[~ x, 1
] = 1.
-
Lemma comm1g x :
[~ 1
, x] = 1.
+
Lemma comm1g x :
[~ 1
, x] = 1.
-
Lemma commgg x :
[~ x, x] = 1.
+
Lemma commgg x :
[~ x, x] = 1.
-
Lemma commgXg x n :
[~ x, x ^+ n] = 1.
+
Lemma commgXg x n :
[~ x, x ^+ n] = 1.
-
Lemma commgVg x :
[~ x, x^-1] = 1.
+
Lemma commgVg x :
[~ x, x^-1] = 1.
-
Lemma commgXVg x n :
[~ x, x ^- n] = 1.
+
Lemma commgXVg x n :
[~ x, x ^- n] = 1.
-Definition gsimp := (mulg1 , mul1g, (invg1, @invgK), (mulgV, mulVg)).
-Definition gnorm := (gsimp, (mulgK, mulgKV, (mulgA, invMg))).
+Definition gsimp := (mulg1 , mul1g, (invg1, @invgK), (mulgV, mulVg)).
+Definition gnorm := (gsimp, (mulgK, mulgKV, (mulgA, invMg))).
@@ -741,22 +740,22 @@
Variable gT : baseFinGroupType.
-Implicit Type A : {set gT}.
+Implicit Type A : {set gT}.
-Definition repr A := if 1 \in A then 1 else odflt 1 [pick x in A].
+Definition repr A := if 1 \in A then 1 else odflt 1 [pick x in A].
-Lemma mem_repr A x : x \in A → repr A \in A.
+Lemma mem_repr A x : x \in A → repr A \in A.
-Lemma card_mem_repr A : #|A| > 0 → repr A \in A.
+Lemma card_mem_repr A : #|A| > 0 → repr A \in A.
-Lemma repr_set1 x : repr [set x] = x.
+Lemma repr_set1 x : repr [set x] = x.
-Lemma repr_set0 : repr set0 = 1.
+Lemma repr_set0 : repr set0 = 1.
End Repr.
@@ -772,7 +771,7 @@
@@ -783,8 +782,8 @@
@@ -795,16 +794,16 @@
@@ -901,10 +900,10 @@
keep all the Notation together.
@@ -914,8 +913,8 @@
the {in ...} form, as in abelian below.
@@ -952,15 +951,15 @@
-
Notation "''N' ( A )" := (
normaliser A) :
group_scope.
-
Notation "''N_' G ( A )" := (
G%
g :&: 'N(A)) :
group_scope.
-
Notation "A <| B" := (
normal A B) :
group_scope.
-
Notation "''C' ( A )" := (
centraliser A) :
group_scope.
-
Notation "''C_' G ( A )" := (
G%
g :&: 'C(A)) :
group_scope.
-
Notation "''C_' ( G ) ( A )" :=
'C_G(A) (
only parsing) :
group_scope.
-
Notation "''C' [ x ]" :=
'N([set x%
g]) :
group_scope.
-
Notation "''C_' G [ x ]" :=
'N_G([set x%
g]) :
group_scope.
-
Notation "''C_' ( G ) [ x ]" :=
'C_G[x] (
only parsing) :
group_scope.
+
Notation "''N' ( A )" := (
normaliser A) :
group_scope.
+
Notation "''N_' G ( A )" := (
G%
g :&: 'N(A)) :
group_scope.
+
Notation "A <| B" := (
normal A B) :
group_scope.
+
Notation "''C' ( A )" := (
centraliser A) :
group_scope.
+
Notation "''C_' G ( A )" := (
G%
g :&: 'C(A)) :
group_scope.
+
Notation "''C_' ( G ) ( A )" :=
'C_G(A) (
only parsing) :
group_scope.
+
Notation "''C' [ x ]" :=
'N([set x%
g]) :
group_scope.
+
Notation "''C_' G [ x ]" :=
'N_G([set x%
g]) :
group_scope.
+
Notation "''C_' ( G ) [ x ]" :=
'C_G[x] (
only parsing) :
group_scope.
@@ -973,7 +972,7 @@
@@ -1031,28 +1030,28 @@
@@ -1063,16 +1062,16 @@
Variable gT :
finGroupType.
-
Implicit Types A B C D :
{set gT}.
+
Implicit Types A B C D :
{set gT}.
Implicit Type x y z :
gT.
@@ -1100,44 +1099,44 @@
@@ -1148,44 +1147,44 @@
@@ -1194,7 +1193,7 @@
Inverse maps lcosets to rcosets
@@ -1205,90 +1204,90 @@
@@ -1299,45 +1298,45 @@
@@ -1348,13 +1347,13 @@
@@ -1365,10 +1364,10 @@
@@ -1379,11 +1378,11 @@
@@ -1419,40 +1418,40 @@
@@ -1504,11 +1503,11 @@
@@ -1541,88 +1540,58 @@
-
Lemma group1 : 1
\in G.
-
Hint Resolve group1.
+
Lemma group1 : 1
\in G.
+
Hint Resolve group1 :
core.
-
-
-
- Loads of silly variants to placate the incompleteness of trivial.
- An alternative would be to upgrade done, pending better support
- in the ssreflect ML code.
-
-
-
-
- Workaround for the fact that the simple matching used by Trivial does not
- always allow conversion. In particular cardG_gt0 always fails to apply to
- subgoals that have been simplified (by /=) because type inference in the
- notation #|G| introduces redexes of the form
- Finite.sort (arg_finGroupType (FinGroup.base gT))
- which get collapsed to Fingroup.arg_sort (FinGroup.base gT).
-
-
@@ -1633,22 +1602,22 @@
@@ -1659,41 +1628,41 @@
-
Lemma groupM x y :
x \in G → y \in G → x × y \in G.
+
Lemma groupM x y :
x \in G → y \in G → x × y \in G.
-
Lemma groupX x n :
x \in G → x ^+ n \in G.
+
Lemma groupX x n :
x \in G → x ^+ n \in G.
-
Lemma groupVr x :
x \in G → x^-1 \in G.
+
Lemma groupVr x :
x \in G → x^-1 \in G.
-
Lemma groupVl x :
x^-1 \in G → x \in G.
+
Lemma groupVl x :
x^-1 \in G → x \in G.
-
Lemma groupV x :
(x^-1 \in G) = (x \in G).
+
Lemma groupV x :
(x^-1 \in G) = (x \in G).
-
Lemma groupMl x y :
x \in G → (x × y \in G) = (y \in G).
+
Lemma groupMl x y :
x \in G → (x × y \in G) = (y \in G).
-
Lemma groupMr x y :
x \in G → (y × x \in G) = (y \in G).
+
Lemma groupMr x y :
x \in G → (y × x \in G) = (y \in G).
-
Definition in_group :=
(group1, groupV, (groupMl, groupX)).
+
Definition in_group :=
(group1, groupV, (groupMl, groupX)).
-
Lemma groupJ x y :
x \in G → y \in G → x ^ y \in G.
+
Lemma groupJ x y :
x \in G → y \in G → x ^ y \in G.
-
Lemma groupJr x y :
y \in G → (x ^ y \in G) = (x \in G).
+
Lemma groupJr x y :
y \in G → (x ^ y \in G) = (x \in G).
-
Lemma groupR x y :
x \in G → y \in G → [~ x, y] \in G.
+
Lemma groupR x y :
x \in G → y \in G → [~ x, y] \in G.
-
Lemma group_prod I r (
P :
pred I)
F :
-
(∀ i,
P i → F i \in G) → \prod_(i <- r | P i) F i \in G.
+
Lemma group_prod I r (
P :
pred I)
F :
+
(∀ i,
P i → F i \in G) → \prod_(i <- r | P i) F i \in G.
@@ -1704,22 +1673,22 @@
@@ -1730,10 +1699,10 @@
@@ -1744,22 +1713,22 @@
@@ -1770,22 +1739,22 @@
@@ -1796,11 +1765,11 @@
@@ -1810,10 +1779,10 @@
(weaker) primitive Coq algorithm for general (co)inductive type families.
@@ -1824,10 +1793,10 @@
@@ -1838,19 +1807,19 @@
@@ -1861,76 +1830,76 @@
@@ -1943,34 +1912,34 @@
@@ -2028,26 +1997,26 @@
-
Lemma group_modl A B G :
A \subset G → A × (B :&: G) = A × B :&: G.
+
Lemma group_modl A B G :
A \subset G → A × (B :&: G) = A × B :&: G.
-
Lemma group_modr A B G :
B \subset G → (G :&: A) × B = G :&: A × B.
+
Lemma group_modr A B G :
B \subset G → (G :&: A) × B = G :&: A × B.
End GroupProp.
-
Hint Resolve group1 group1_class1 group1_class12 group1_class12.
-
Hint Resolve group1_eqType group1_finType.
-
Hint Resolve cardG_gt0 cardG_gt0_reduced indexg_gt0.
+
Hint Extern 0 (
is_true (1%
g \in _)) ⇒
apply:
group1 :
core.
+
Hint Extern 0 (
is_true (0
< #|_|)) ⇒
apply:
cardG_gt0 :
core.
+
Hint Extern 0 (
is_true (0
< #|_ : _|)) ⇒
apply:
indexg_gt0 :
core.
-
Notation "G :^ x" := (
conjG_group G x) :
Group_scope.
+
Notation "G :^ x" := (
conjG_group G x) :
Group_scope.
-
Notation "[ 'subg' G ]" := (
subg_of G) :
type_scope.
-
Notation "[ 'subg' G ]" :=
[set: subg_of G] :
group_scope.
-
Notation "[ 'subg' G ]" :=
[set: subg_of G]%
G :
Group_scope.
+
Notation "[ 'subg' G ]" := (
subg_of G) :
type_scope.
+
Notation "[ 'subg' G ]" :=
[set: subg_of G] :
group_scope.
+
Notation "[ 'subg' G ]" :=
[set: subg_of G]%
G :
Group_scope.
@@ -2058,11 +2027,11 @@
Variable gT :
finGroupType.
-
Implicit Types A B :
{set gT}.
-
Implicit Types G H :
{group gT}.
+
Implicit Types A B :
{set gT}.
+
Implicit Types G H :
{group gT}.
-
Lemma group_setI G H :
group_set (
G :&: H).
+
Lemma group_setI G H :
group_set (
G :&: H).
Canonical setI_group G H :=
group (
group_setI G H).
@@ -2071,10 +2040,10 @@
Section Nary.
-
Variables (
I :
finType) (
P :
pred I) (
F :
I → {group gT}).
+
Variables (
I :
finType) (
P :
pred I) (
F :
I → {group gT}).
-
Lemma group_set_bigcap :
group_set (
\bigcap_(i | P i) F i).
+
Lemma group_set_bigcap :
group_set (
\bigcap_(i | P i) F i).
Canonical bigcap_group :=
group group_set_bigcap.
@@ -2083,189 +2052,189 @@
End Nary.
-
Canonical generated_group A :
{group _} :=
Eval hnf in [group of <<A>>].
-
Canonical gcore_group G A :
{group _} :=
Eval hnf in [group of gcore G A].
-
Canonical commutator_group A B :
{group _} :=
Eval hnf in [group of [~: A, B]].
-
Canonical joing_group A B :
{group _} :=
Eval hnf in [group of A <*> B].
-
Canonical cycle_group x :
{group _} :=
Eval hnf in [group of <[x]>].
+
Canonical generated_group A :
{group _} :=
Eval hnf in [group of <<A>>].
+
Canonical gcore_group G A :
{group _} :=
Eval hnf in [group of gcore G A].
+
Canonical commutator_group A B :
{group _} :=
Eval hnf in [group of [~: A, B]].
+
Canonical joing_group A B :
{group _} :=
Eval hnf in [group of A <*> B].
+
Canonical cycle_group x :
{group _} :=
Eval hnf in [group of <[x]>].
Definition joinG G H :=
joing_group G H.
-
Definition subgroups A :=
[set G : {group gT} | G \subset A].
+
Definition subgroups A :=
[set G : {group gT} | G \subset A].
-
Lemma order_gt0 (
x :
gT) : 0
< #[x].
+
Lemma order_gt0 (
x :
gT) : 0
< #[x].
End GroupInter.
-
Hint Resolve order_gt0.
+
Hint Resolve order_gt0 :
core.
-
Notation "G :&: H" := (
setI_group G H) :
Group_scope.
-
Notation "<< A >>" := (
generated_group A) :
Group_scope.
-
Notation "<[ x ] >" := (
cycle_group x) :
Group_scope.
-
Notation "[ ~: A1 , A2 , .. , An ]" :=
+
Notation "G :&: H" := (
setI_group G H) :
Group_scope.
+
Notation "<< A >>" := (
generated_group A) :
Group_scope.
+
Notation "<[ x ] >" := (
cycle_group x) :
Group_scope.
+
Notation "[ ~: A1 , A2 , .. , An ]" :=
(
commutator_group .. (
commutator_group A1 A2) ..
An) :
Group_scope.
-
Notation "A <*> B" := (
joing_group A B) :
Group_scope.
-
Notation "G * H" := (
joinG G H) :
Group_scope.
-
-
-
Notation "\prod_ ( i <- r | P ) F" :=
- (
\big[joinG/1%
G]_(i <- r | P%
B) F%
G) :
Group_scope.
-
Notation "\prod_ ( i <- r ) F" :=
- (
\big[joinG/1%
G]_(i <- r) F%
G) :
Group_scope.
-
Notation "\prod_ ( m <= i < n | P ) F" :=
- (
\big[joinG/1%
G]_(m ≤ i < n | P%
B) F%
G) :
Group_scope.
-
Notation "\prod_ ( m <= i < n ) F" :=
- (
\big[joinG/1%
G]_(m ≤ i < n) F%
G) :
Group_scope.
-
Notation "\prod_ ( i | P ) F" :=
- (
\big[joinG/1%
G]_(i | P%
B) F%
G) :
Group_scope.
-
Notation "\prod_ i F" :=
- (
\big[joinG/1%
G]_i F%
G) :
Group_scope.
-
Notation "\prod_ ( i : t | P ) F" :=
- (
\big[joinG/1%
G]_(i : t | P%
B) F%
G) (
only parsing) :
Group_scope.
-
Notation "\prod_ ( i : t ) F" :=
- (
\big[joinG/1%
G]_(i : t) F%
G) (
only parsing) :
Group_scope.
-
Notation "\prod_ ( i < n | P ) F" :=
- (
\big[joinG/1%
G]_(i < n | P%
B) F%
G) :
Group_scope.
-
Notation "\prod_ ( i < n ) F" :=
- (
\big[joinG/1%
G]_(i < n) F%
G) :
Group_scope.
-
Notation "\prod_ ( i 'in' A | P ) F" :=
- (
\big[joinG/1%
G]_(i in A | P%
B) F%
G) :
Group_scope.
-
Notation "\prod_ ( i 'in' A ) F" :=
- (
\big[joinG/1%
G]_(i in A) F%
G) :
Group_scope.
+
Notation "A <*> B" := (
joing_group A B) :
Group_scope.
+
Notation "G * H" := (
joinG G H) :
Group_scope.
+
+
+
Notation "\prod_ ( i <- r | P ) F" :=
+ (
\big[joinG/1%
G]_(i <- r | P%
B) F%
G) :
Group_scope.
+
Notation "\prod_ ( i <- r ) F" :=
+ (
\big[joinG/1%
G]_(i <- r) F%
G) :
Group_scope.
+
Notation "\prod_ ( m <= i < n | P ) F" :=
+ (
\big[joinG/1%
G]_(m ≤ i < n | P%
B) F%
G) :
Group_scope.
+
Notation "\prod_ ( m <= i < n ) F" :=
+ (
\big[joinG/1%
G]_(m ≤ i < n) F%
G) :
Group_scope.
+
Notation "\prod_ ( i | P ) F" :=
+ (
\big[joinG/1%
G]_(i | P%
B) F%
G) :
Group_scope.
+
Notation "\prod_ i F" :=
+ (
\big[joinG/1%
G]_i F%
G) :
Group_scope.
+
Notation "\prod_ ( i : t | P ) F" :=
+ (
\big[joinG/1%
G]_(i : t | P%
B) F%
G) (
only parsing) :
Group_scope.
+
Notation "\prod_ ( i : t ) F" :=
+ (
\big[joinG/1%
G]_(i : t) F%
G) (
only parsing) :
Group_scope.
+
Notation "\prod_ ( i < n | P ) F" :=
+ (
\big[joinG/1%
G]_(i < n | P%
B) F%
G) :
Group_scope.
+
Notation "\prod_ ( i < n ) F" :=
+ (
\big[joinG/1%
G]_(i < n) F%
G) :
Group_scope.
+
Notation "\prod_ ( i 'in' A | P ) F" :=
+ (
\big[joinG/1%
G]_(i in A | P%
B) F%
G) :
Group_scope.
+
Notation "\prod_ ( i 'in' A ) F" :=
+ (
\big[joinG/1%
G]_(i in A) F%
G) :
Group_scope.
Section Lagrange.
Variable gT :
finGroupType.
-
Implicit Types G H K :
{group gT}.
+
Implicit Types G H K :
{group gT}.
-
Lemma LagrangeI G H : (
#|G :&: H| × #|G : H|)%
N = #|G|.
+
Lemma LagrangeI G H : (
#|G :&: H| × #|G : H|)%
N = #|G|.
-
Lemma divgI G H :
#|G| %/ #|G :&: H| = #|G : H|.
+
Lemma divgI G H :
#|G| %/ #|G :&: H| = #|G : H|.
-
Lemma divg_index G H :
#|G| %/ #|G : H| = #|G :&: H|.
+
Lemma divg_index G H :
#|G| %/ #|G : H| = #|G :&: H|.
-
Lemma dvdn_indexg G H :
#|G : H| %| #|G|.
+
Lemma dvdn_indexg G H :
#|G : H| %| #|G|.
-
Theorem Lagrange G H :
H \subset G → (
#|H| × #|G : H|)%
N = #|G|.
+
Theorem Lagrange G H :
H \subset G → (
#|H| × #|G : H|)%
N = #|G|.
-
Lemma cardSg G H :
H \subset G → #|H| %| #|G|.
+
Lemma cardSg G H :
H \subset G → #|H| %| #|G|.
-
Lemma lognSg p G H :
G \subset H → logn p #|G| ≤ logn p #|H|.
+
Lemma lognSg p G H :
G \subset H → logn p #|G| ≤ logn p #|H|.
-
Lemma piSg G H :
G \subset H → {subset \pi(gval G) ≤ \pi(gval H)}.
+
Lemma piSg G H :
G \subset H → {subset \pi(gval G) ≤ \pi(gval H)}.
-
Lemma divgS G H :
H \subset G → #|G| %/ #|H| = #|G : H|.
+
Lemma divgS G H :
H \subset G → #|G| %/ #|H| = #|G : H|.
-
Lemma divg_indexS G H :
H \subset G → #|G| %/ #|G : H| = #|H|.
+
Lemma divg_indexS G H :
H \subset G → #|G| %/ #|G : H| = #|H|.
-
Lemma coprimeSg G H p :
H \subset G → coprime #|G| p → coprime #|H| p.
+
Lemma coprimeSg G H p :
H \subset G → coprime #|G| p → coprime #|H| p.
-
Lemma coprimegS G H p :
H \subset G → coprime p #|G| → coprime p #|H|.
+
Lemma coprimegS G H p :
H \subset G → coprime p #|G| → coprime p #|H|.
-
Lemma indexJg G H x :
#|G :^ x : H :^ x| = #|G : H|.
+
Lemma indexJg G H x :
#|G :^ x : H :^ x| = #|G : H|.
-
Lemma indexgg G :
#|G : G| = 1%
N.
+
Lemma indexgg G :
#|G : G| = 1%
N.
-
Lemma rcosets_id G :
rcosets G G = [set G : {set gT}].
+
Lemma rcosets_id G :
rcosets G G = [set G : {set gT}].
Lemma Lagrange_index G H K :
-
H \subset G → K \subset H → (
#|G : H| × #|H : K|)%
N = #|G : K|.
+
H \subset G → K \subset H → (
#|G : H| × #|H : K|)%
N = #|G : K|.
-
Lemma indexgI G H :
#|G : G :&: H| = #|G : H|.
+
Lemma indexgI G H :
#|G : G :&: H| = #|G : H|.
-
Lemma indexgS G H K :
H \subset K → #|G : K| %| #|G : H|.
+
Lemma indexgS G H K :
H \subset K → #|G : K| %| #|G : H|.
-
Lemma indexSg G H K :
H \subset K → K \subset G → #|K : H| %| #|G : H|.
+
Lemma indexSg G H K :
H \subset K → K \subset G → #|K : H| %| #|G : H|.
-
Lemma indexg_eq1 G H :
(#|G : H| == 1%
N) = (G \subset H).
+
Lemma indexg_eq1 G H :
(#|G : H| == 1%
N) = (G \subset H).
-
Lemma indexg_gt1 G H :
(#|G : H| > 1
) = ~~ (G \subset H).
+
Lemma indexg_gt1 G H :
(#|G : H| > 1
) = ~~ (G \subset H).
-
Lemma index1g G H :
H \subset G → #|G : H| = 1%
N → H :=: G.
+
Lemma index1g G H :
H \subset G → #|G : H| = 1%
N → H :=: G.
-
Lemma indexg1 G :
#|G : 1
| = #|G|.
+
Lemma indexg1 G :
#|G : 1
| = #|G|.
-
Lemma indexMg G A :
#|G × A : G| = #|A : G|.
+
Lemma indexMg G A :
#|G × A : G| = #|A : G|.
-
Lemma rcosets_partition_mul G H :
partition (
rcosets H G) (
H × G).
+
Lemma rcosets_partition_mul G H :
partition (
rcosets H G) (
H × G).
-
Lemma rcosets_partition G H :
H \subset G → partition (
rcosets H G)
G.
+
Lemma rcosets_partition G H :
H \subset G → partition (
rcosets H G)
G.
-
Lemma LagrangeMl G H : (
#|G| × #|H : G|)%
N = #|G × H|.
+
Lemma LagrangeMl G H : (
#|G| × #|H : G|)%
N = #|G × H|.
-
Lemma LagrangeMr G H : (
#|G : H| × #|H|)%
N = #|G × H|.
+
Lemma LagrangeMr G H : (
#|G : H| × #|H|)%
N = #|G × H|.
-
Lemma mul_cardG G H : (
#|G| × #|H| = #|G × H|%
g × #|G :&: H|)%
N.
+
Lemma mul_cardG G H : (
#|G| × #|H| = #|G × H|%
g × #|G :&: H|)%
N.
-
Lemma dvdn_cardMg G H :
#|G × H| %| #|G| × #|H|.
+
Lemma dvdn_cardMg G H :
#|G × H| %| #|G| × #|H|.
-
Lemma cardMg_divn G H :
#|G × H| = (#|G| × #|H|) %/ #|G :&: H|.
+
Lemma cardMg_divn G H :
#|G × H| = (#|G| × #|H|) %/ #|G :&: H|.
-
Lemma cardIg_divn G H :
#|G :&: H| = (#|G| × #|H|) %/ #|G × H|.
+
Lemma cardIg_divn G H :
#|G :&: H| = (#|G| × #|H|) %/ #|G × H|.
-
Lemma TI_cardMg G H :
G :&: H = 1
→ #|G × H| = (
#|G| × #|H|)%
N.
+
Lemma TI_cardMg G H :
G :&: H = 1
→ #|G × H| = (
#|G| × #|H|)%
N.
-
Lemma cardMg_TI G H :
#|G| × #|H| ≤ #|G × H| → G :&: H = 1.
+
Lemma cardMg_TI G H :
#|G| × #|H| ≤ #|G × H| → G :&: H = 1.
-
Lemma coprime_TIg G H :
coprime #|G| #|H| → G :&: H = 1.
+
Lemma coprime_TIg G H :
coprime #|G| #|H| → G :&: H = 1.
-
Lemma prime_TIg G H :
prime #|G| → ~~ (G \subset H) → G :&: H = 1.
+
Lemma prime_TIg G H :
prime #|G| → ~~ (G \subset H) → G :&: H = 1.
-
Lemma prime_meetG G H :
prime #|G| → G :&: H != 1
→ G \subset H.
+
Lemma prime_meetG G H :
prime #|G| → G :&: H != 1
→ G \subset H.
-
Lemma coprime_cardMg G H :
coprime #|G| #|H| → #|G × H| = (
#|G| × #|H|)%
N.
+
Lemma coprime_cardMg G H :
coprime #|G| #|H| → #|G × H| = (
#|G| × #|H|)%
N.
Lemma coprime_index_mulG G H K :
-
H \subset G → K \subset G → coprime #|G : H| #|G : K| → H × K = G.
+
H \subset G → K \subset G → coprime #|G : H| #|G : K| → H × K = G.
End Lagrange.
@@ -2276,184 +2245,184 @@
Variable gT :
finGroupType.
Implicit Types x y z :
gT.
-
Implicit Types A B C D :
{set gT}.
-
Implicit Types G H K :
{group gT}.
+
Implicit Types A B C D :
{set gT}.
+
Implicit Types G H K :
{group gT}.
-
Lemma subset_gen A :
A \subset <<A>>.
+
Lemma subset_gen A :
A \subset <<A>>.
-
Lemma sub_gen A B :
A \subset B → A \subset <<B>>.
+
Lemma sub_gen A B :
A \subset B → A \subset <<B>>.
-
Lemma mem_gen x A :
x \in A → x \in <<A>>.
+
Lemma mem_gen x A :
x \in A → x \in <<A>>.
-
Lemma generatedP x A :
reflect (
∀ G,
A \subset G → x \in G) (
x \in <<A>>).
+
Lemma generatedP x A :
reflect (
∀ G,
A \subset G → x \in G) (
x \in <<A>>).
-
Lemma gen_subG A G :
(<<A>> \subset G) = (A \subset G).
+
Lemma gen_subG A G :
(<<A>> \subset G) = (A \subset G).
-
Lemma genGid G :
<<G>> = G.
+
Lemma genGid G :
<<G>> = G.
-
Lemma genGidG G :
<<G>>%
G = G.
+
Lemma genGidG G :
<<G>>%
G = G.
-
Lemma gen_set_id A :
group_set A → <<A>> = A.
+
Lemma gen_set_id A :
group_set A → <<A>> = A.
-
Lemma genS A B :
A \subset B → <<A>> \subset <<B>>.
+
Lemma genS A B :
A \subset B → <<A>> \subset <<B>>.
-
Lemma gen0 :
<<set0>> = 1
:> {set gT}.
+
Lemma gen0 :
<<set0>> = 1
:> {set gT}.
-
Lemma gen_expgs A :
{n | <<A>> = (1
|: A) ^+ n}.
+
Lemma gen_expgs A :
{n | <<A>> = (1
|: A) ^+ n}.
Lemma gen_prodgP A x :
-
reflect (
∃ n, exists2 c, ∀ i :
'I_n,
c i \in A & x = \prod_i c i)
- (
x \in <<A>>).
+
reflect (
∃ n, exists2 c, ∀ i :
'I_n,
c i \in A & x = \prod_i c i)
+ (
x \in <<A>>).
-
Lemma genD A B :
A \subset <<A :\: B>> → <<A :\: B>> = <<A>>.
+
Lemma genD A B :
A \subset <<A :\: B>> → <<A :\: B>> = <<A>>.
-
Lemma genV A :
<<A^-1>> = <<A>>.
+
Lemma genV A :
<<A^-1>> = <<A>>.
-
Lemma genJ A z :
<<A :^z>> = <<A>> :^ z.
+
Lemma genJ A z :
<<A :^z>> = <<A>> :^ z.
-
Lemma conjYg A B z :
(A <*> B) :^z = A :^ z <*> B :^ z.
+
Lemma conjYg A B z :
(A <*> B) :^z = A :^ z <*> B :^ z.
-
Lemma genD1 A x :
x \in <<A :\ x>> → <<A :\ x>> = <<A>>.
+
Lemma genD1 A x :
x \in <<A :\ x>> → <<A :\ x>> = <<A>>.
-
Lemma genD1id A :
<<A^#>> = <<A>>.
+
Lemma genD1id A :
<<A^#>> = <<A>>.
Notation joingT := (@
joing gT) (
only parsing).
Notation joinGT := (@
joinG gT) (
only parsing).
-
Lemma joingE A B :
A <*> B = <<A :|: B>>.
+
Lemma joingE A B :
A <*> B = <<A :|: B>>.
-
Lemma joinGE G H : (
G × H)%
G = (
G <*> H)%
G.
+
Lemma joinGE G H : (
G × H)%
G = (
G <*> H)%
G.
-
Lemma joingC :
commutative joingT.
+
Lemma joingC :
commutative joingT.
-
Lemma joing_idr A B :
A <*> <<B>> = A <*> B.
+
Lemma joing_idr A B :
A <*> <<B>> = A <*> B.
-
Lemma joing_idl A B :
<<A>> <*> B = A <*> B.
+
Lemma joing_idl A B :
<<A>> <*> B = A <*> B.
-
Lemma joing_subl A B :
A \subset A <*> B.
+
Lemma joing_subl A B :
A \subset A <*> B.
-
Lemma joing_subr A B :
B \subset A <*> B.
+
Lemma joing_subr A B :
B \subset A <*> B.
-
Lemma join_subG A B G :
(A <*> B \subset G) = (A \subset G) && (B \subset G).
+
Lemma join_subG A B G :
(A <*> B \subset G) = (A \subset G) && (B \subset G).
-
Lemma joing_idPl G A :
reflect (
G <*> A = G) (
A \subset G).
+
Lemma joing_idPl G A :
reflect (
G <*> A = G) (
A \subset G).
-
Lemma joing_idPr A G :
reflect (
A <*> G = G) (
A \subset G).
+
Lemma joing_idPr A G :
reflect (
A <*> G = G) (
A \subset G).
Lemma joing_subP A B G :
-
reflect (
A \subset G ∧ B \subset G) (
A <*> B \subset G).
+
reflect (
A \subset G ∧ B \subset G) (
A <*> B \subset G).
-
Lemma joing_sub A B C :
A <*> B = C → A \subset C ∧ B \subset C.
+
Lemma joing_sub A B C :
A <*> B = C → A \subset C ∧ B \subset C.
-
Lemma genDU A B C :
A \subset C → <<C :\: A>> = <<B>> → <<A :|: B>> = <<C>>.
+
Lemma genDU A B C :
A \subset C → <<C :\: A>> = <<B>> → <<A :|: B>> = <<C>>.
-
Lemma joingA :
associative joingT.
+
Lemma joingA :
associative joingT.
-
Lemma joing1G G : 1
<*> G = G.
+
Lemma joing1G G : 1
<*> G = G.
-
Lemma joingG1 G :
G <*> 1
= G.
+
Lemma joingG1 G :
G <*> 1
= G.
-
Lemma genM_join G H :
<<G × H>> = G <*> H.
+
Lemma genM_join G H :
<<G × H>> = G <*> H.
-
Lemma mulG_subG G H K :
(G × H \subset K) = (G \subset K) && (H \subset K).
+
Lemma mulG_subG G H K :
(G × H \subset K) = (G \subset K) && (H \subset K).
-
Lemma mulGsubP K H G :
reflect (
K \subset G ∧ H \subset G) (
K × H \subset G).
+
Lemma mulGsubP K H G :
reflect (
K \subset G ∧ H \subset G) (
K × H \subset G).
-
Lemma mulG_sub K H A :
K × H = A → K \subset A ∧ H \subset A.
+
Lemma mulG_sub K H A :
K × H = A → K \subset A ∧ H \subset A.
-
Lemma trivMg G H :
(G × H == 1
) = (G :==: 1
) && (H :==: 1
).
+
Lemma trivMg G H :
(G × H == 1
) = (G :==: 1
) && (H :==: 1
).
-
Lemma comm_joingE G H :
commute G H → G <*> H = G × H.
+
Lemma comm_joingE G H :
commute G H → G <*> H = G × H.
-
Lemma joinGC :
commutative joinGT.
+
Lemma joinGC :
commutative joinGT.
-
Lemma joinGA :
associative joinGT.
+
Lemma joinGA :
associative joinGT.
-
Lemma join1G :
left_id 1%
G joinGT.
+
Lemma join1G :
left_id 1%
G joinGT.
-
Lemma joinG1 :
right_id 1%
G joinGT.
+
Lemma joinG1 :
right_id 1%
G joinGT.
Canonical joinG_law :=
Monoid.Law joinGA join1G joinG1.
Canonical joinG_abelaw :=
Monoid.ComLaw joinGC.
-
Lemma bigprodGEgen I r (
P :
pred I) (
F :
I → {set gT}) :
- (
\prod_(i <- r | P i) <<F i>>)%
G :=: << \bigcup_(i <- r | P i) F i >>.
+
Lemma bigprodGEgen I r (
P :
pred I) (
F :
I → {set gT}) :
+ (
\prod_(i <- r | P i) <<F i>>)%
G :=: << \bigcup_(i <- r | P i) F i >>.
-
Lemma bigprodGE I r (
P :
pred I) (
F :
I → {group gT}) :
- (
\prod_(i <- r | P i) F i)%
G :=: << \bigcup_(i <- r | P i) F i >>.
+
Lemma bigprodGE I r (
P :
pred I) (
F :
I → {group gT}) :
+ (
\prod_(i <- r | P i) F i)%
G :=: << \bigcup_(i <- r | P i) F i >>.
-
Lemma mem_commg A B x y :
x \in A → y \in B → [~ x, y] \in [~: A, B].
+
Lemma mem_commg A B x y :
x \in A → y \in B → [~ x, y] \in [~: A, B].
-
Lemma commSg A B C :
A \subset B → [~: A, C] \subset [~: B, C].
+
Lemma commSg A B C :
A \subset B → [~: A, C] \subset [~: B, C].
-
Lemma commgS A B C :
B \subset C → [~: A, B] \subset [~: A, C].
+
Lemma commgS A B C :
B \subset C → [~: A, B] \subset [~: A, C].
Lemma commgSS A B C D :
-
A \subset B → C \subset D → [~: A, C] \subset [~: B, D].
+
A \subset B → C \subset D → [~: A, C] \subset [~: B, D].
-
Lemma der1_subG G :
[~: G, G] \subset G.
+
Lemma der1_subG G :
[~: G, G] \subset G.
-
Lemma comm_subG A B G :
A \subset G → B \subset G → [~: A, B] \subset G.
+
Lemma comm_subG A B G :
A \subset G → B \subset G → [~: A, B] \subset G.
-
Lemma commGC A B :
[~: A, B] = [~: B, A].
+
Lemma commGC A B :
[~: A, B] = [~: B, A].
-
Lemma conjsRg A B x :
[~: A, B] :^ x = [~: A :^ x, B :^ x].
+
Lemma conjsRg A B x :
[~: A, B] :^ x = [~: A :^ x, B :^ x].
End GeneratedGroup.
@@ -2476,79 +2445,79 @@
Variable gT :
finGroupType.
Implicit Types x y :
gT.
-
Implicit Types G :
{group gT}.
+
Implicit Types G :
{group gT}.
Import Monoid.Theory.
-
Lemma cycle1 :
<[1
]> = [1 gT].
+
Lemma cycle1 :
<[1
]> = [1 gT].
-
Lemma order1 :
#[1
: gT] = 1%
N.
+
Lemma order1 :
#[1
: gT] = 1%
N.
-
Lemma cycle_id x :
x \in <[x]>.
+
Lemma cycle_id x :
x \in <[x]>.
-
Lemma mem_cycle x i :
x ^+ i \in <[x]>.
+
Lemma mem_cycle x i :
x ^+ i \in <[x]>.
-
Lemma cycle_subG x G :
(<[x]> \subset G) = (x \in G).
+
Lemma cycle_subG x G :
(<[x]> \subset G) = (x \in G).
-
Lemma cycle_eq1 x :
(<[x]> == 1
) = (x == 1
).
+
Lemma cycle_eq1 x :
(<[x]> == 1
) = (x == 1
).
-
Lemma orderE x :
#[x] = #|<[x]>|.
+
Lemma orderE x :
#[x] = #|<[x]>|.
-
Lemma order_eq1 x :
(#[x] == 1%
N) = (x == 1
).
+
Lemma order_eq1 x :
(#[x] == 1%
N) = (x == 1
).
-
Lemma order_gt1 x :
(#[x] > 1
) = (x != 1
).
+
Lemma order_gt1 x :
(#[x] > 1
) = (x != 1
).
-
Lemma cycle_traject x :
<[x]> =i traject (
mulg x) 1
#[x].
+
Lemma cycle_traject x :
<[x]> =i traject (
mulg x) 1
#[x].
-
Lemma cycle2g x :
#[x] = 2
→ <[x]> = [set 1
; x].
+
Lemma cycle2g x :
#[x] = 2
→ <[x]> = [set 1
; x].
-
Lemma cyclePmin x y :
y \in <[x]> → {i | i < #[x] & y = x ^+ i}.
+
Lemma cyclePmin x y :
y \in <[x]> → {i | i < #[x] & y = x ^+ i}.
-
Lemma cycleP x y :
reflect (
∃ i, y = x ^+ i) (
y \in <[x]>).
+
Lemma cycleP x y :
reflect (
∃ i, y = x ^+ i) (
y \in <[x]>).
-
Lemma expg_order x :
x ^+ #[x] = 1.
+
Lemma expg_order x :
x ^+ #[x] = 1.
-
Lemma expg_mod p k x :
x ^+ p = 1
→ x ^+ (k %% p) = x ^+ k.
+
Lemma expg_mod p k x :
x ^+ p = 1
→ x ^+ (k %% p) = x ^+ k.
-
Lemma expg_mod_order x i :
x ^+ (i %% #[x]) = x ^+ i.
+
Lemma expg_mod_order x i :
x ^+ (i %% #[x]) = x ^+ i.
-
Lemma invg_expg x :
x^-1 = x ^+ #[x].-1.
+
Lemma invg_expg x :
x^-1 = x ^+ #[x].-1.
-
Lemma invg2id x :
#[x] = 2
→ x^-1 = x.
+
Lemma invg2id x :
#[x] = 2
→ x^-1 = x.
-
Lemma cycleX x i :
<[x ^+ i]> \subset <[x]>.
+
Lemma cycleX x i :
<[x ^+ i]> \subset <[x]>.
-
Lemma cycleV x :
<[x^-1]> = <[x]>.
+
Lemma cycleV x :
<[x^-1]> = <[x]>.
-
Lemma orderV x :
#[x^-1] = #[x].
+
Lemma orderV x :
#[x^-1] = #[x].
-
Lemma cycleJ x y :
<[x ^ y]> = <[x]> :^ y.
+
Lemma cycleJ x y :
<[x ^ y]> = <[x]> :^ y.
-
Lemma orderJ x y :
#[x ^ y] = #[x].
+
Lemma orderJ x y :
#[x ^ y] = #[x].
End Cycles.
@@ -2559,217 +2528,217 @@
Variable gT :
finGroupType.
Implicit Types x y z :
gT.
-
Implicit Types A B C D :
{set gT}.
-
Implicit Type G H K :
{group gT}.
+
Implicit Types A B C D :
{set gT}.
+
Implicit Type G H K :
{group gT}.
-
Lemma normP x A :
reflect (
A :^ x = A) (
x \in 'N(A)).
+
Lemma normP x A :
reflect (
A :^ x = A) (
x \in 'N(A)).
-
Lemma group_set_normaliser A :
group_set 'N(A).
+
Lemma group_set_normaliser A :
group_set 'N(A).
Canonical normaliser_group A :=
group (
group_set_normaliser A).
-
Lemma normsP A B :
reflect {in A, normalised B} (
A \subset 'N(B)).
+
Lemma normsP A B :
reflect {in A, normalised B} (
A \subset 'N(B)).
-
Lemma memJ_norm x y A :
x \in 'N(A) → (y ^ x \in A) = (y \in A).
+
Lemma memJ_norm x y A :
x \in 'N(A) → (y ^ x \in A) = (y \in A).
-
Lemma norms_cycle x y :
(<[y]> \subset 'N(<[x]>)) = (x ^ y \in <[x]>).
+
Lemma norms_cycle x y :
(<[y]> \subset 'N(<[x]>)) = (x ^ y \in <[x]>).
-
Lemma norm1 :
'N(1
) = setT :> {set gT}.
+
Lemma norm1 :
'N(1
) = setT :> {set gT}.
-
Lemma norms1 A :
A \subset 'N(1
).
+
Lemma norms1 A :
A \subset 'N(1
).
-
Lemma normCs A :
'N(~: A) = 'N(A).
+
Lemma normCs A :
'N(~: A) = 'N(A).
-
Lemma normG G :
G \subset 'N(G).
+
Lemma normG G :
G \subset 'N(G).
-
Lemma normT :
'N([set: gT]) = [set: gT].
+
Lemma normT :
'N([set: gT]) = [set: gT].
-
Lemma normsG A G :
A \subset G → A \subset 'N(G).
+
Lemma normsG A G :
A \subset G → A \subset 'N(G).
-
Lemma normC A B :
A \subset 'N(B) → commute A B.
+
Lemma normC A B :
A \subset 'N(B) → commute A B.
-
Lemma norm_joinEl G H :
G \subset 'N(H) → G <*> H = G × H.
+
Lemma norm_joinEl G H :
G \subset 'N(H) → G <*> H = G × H.
-
Lemma norm_joinEr G H :
H \subset 'N(G) → G <*> H = G × H.
+
Lemma norm_joinEr G H :
H \subset 'N(G) → G <*> H = G × H.
-
Lemma norm_rlcoset G x :
x \in 'N(G) → G :* x = x *: G.
+
Lemma norm_rlcoset G x :
x \in 'N(G) → G :* x = x *: G.
-
Lemma rcoset_mul G x y :
x \in 'N(G) → (G :* x) × (G :* y) = G :* (x × y).
+
Lemma rcoset_mul G x y :
x \in 'N(G) → (G :* x) × (G :* y) = G :* (x × y).
-
Lemma normJ A x :
'N(A :^ x) = 'N(A) :^ x.
+
Lemma normJ A x :
'N(A :^ x) = 'N(A) :^ x.
Lemma norm_conj_norm x A B :
-
x \in 'N(A) → (A \subset 'N(B :^ x)) = (A \subset 'N(B)).
+
x \in 'N(A) → (A \subset 'N(B :^ x)) = (A \subset 'N(B)).
-
Lemma norm_gen A :
'N(A) \subset 'N(<<A>>).
+
Lemma norm_gen A :
'N(A) \subset 'N(<<A>>).
-
Lemma class_norm x G :
G \subset 'N(x ^: G).
+
Lemma class_norm x G :
G \subset 'N(x ^: G).
-
Lemma class_normal x G :
x \in G → x ^: G <| G.
+
Lemma class_normal x G :
x \in G → x ^: G <| G.
-
Lemma class_sub_norm G A x :
G \subset 'N(A) → (x ^: G \subset A) = (x \in A).
+
Lemma class_sub_norm G A x :
G \subset 'N(A) → (x ^: G \subset A) = (x \in A).
-
Lemma class_support_norm A G :
G \subset 'N(class_support A G).
+
Lemma class_support_norm A G :
G \subset 'N(class_support A G).
Lemma class_support_sub_norm A B G :
-
A \subset G → B \subset 'N(G) → class_support A B \subset G.
+
A \subset G → B \subset 'N(G) → class_support A B \subset G.
Section norm_trans.
-
Variables (
A B C D :
{set gT}).
-
Hypotheses (
nBA :
A \subset 'N(B)) (
nCA :
A \subset 'N(C)).
+
Variables (
A B C D :
{set gT}).
+
Hypotheses (
nBA :
A \subset 'N(B)) (
nCA :
A \subset 'N(C)).
-
Lemma norms_gen :
A \subset 'N(<<B>>).
+
Lemma norms_gen :
A \subset 'N(<<B>>).
-
Lemma norms_norm :
A \subset 'N('N(B)).
+
Lemma norms_norm :
A \subset 'N('N(B)).
-
Lemma normsI :
A \subset 'N(B :&: C).
+
Lemma normsI :
A \subset 'N(B :&: C).
-
Lemma normsU :
A \subset 'N(B :|: C).
+
Lemma normsU :
A \subset 'N(B :|: C).
-
Lemma normsIs :
B \subset 'N(D) → A :&: B \subset 'N(C :&: D).
+
Lemma normsIs :
B \subset 'N(D) → A :&: B \subset 'N(C :&: D).
-
Lemma normsD :
A \subset 'N(B :\: C).
+
Lemma normsD :
A \subset 'N(B :\: C).
-
Lemma normsM :
A \subset 'N(B × C).
+
Lemma normsM :
A \subset 'N(B × C).
-
Lemma normsY :
A \subset 'N(B <*> C).
+
Lemma normsY :
A \subset 'N(B <*> C).
-
Lemma normsR :
A \subset 'N([~: B, C]).
+
Lemma normsR :
A \subset 'N([~: B, C]).
-
Lemma norms_class_support :
A \subset 'N(class_support B C).
+
Lemma norms_class_support :
A \subset 'N(class_support B C).
End norm_trans.
-
Lemma normsIG A B G :
A \subset 'N(B) → A :&: G \subset 'N(B :&: G).
+
Lemma normsIG A B G :
A \subset 'N(B) → A :&: G \subset 'N(B :&: G).
-
Lemma normsGI A B G :
A \subset 'N(B) → G :&: A \subset 'N(G :&: B).
+
Lemma normsGI A B G :
A \subset 'N(B) → G :&: A \subset 'N(G :&: B).
-
Lemma norms_bigcap I r (
P :
pred I)
A (
B_ :
I → {set gT}) :
-
A \subset \bigcap_(i <- r | P i) 'N(B_ i) →
-
A \subset 'N(\bigcap_(i <- r | P i) B_ i).
+
Lemma norms_bigcap I r (
P :
pred I)
A (
B_ :
I → {set gT}) :
+
A \subset \bigcap_(i <- r | P i) 'N(B_ i) →
+
A \subset 'N(\bigcap_(i <- r | P i) B_ i).
-
Lemma norms_bigcup I r (
P :
pred I)
A (
B_ :
I → {set gT}) :
-
A \subset \bigcap_(i <- r | P i) 'N(B_ i) →
-
A \subset 'N(\bigcup_(i <- r | P i) B_ i).
+
Lemma norms_bigcup I r (
P :
pred I)
A (
B_ :
I → {set gT}) :
+
A \subset \bigcap_(i <- r | P i) 'N(B_ i) →
+
A \subset 'N(\bigcup_(i <- r | P i) B_ i).
-
Lemma normsD1 A B :
A \subset 'N(B) → A \subset 'N(B^#).
+
Lemma normsD1 A B :
A \subset 'N(B) → A \subset 'N(B^#).
-
Lemma normD1 A :
'N(A^#) = 'N(A).
+
Lemma normD1 A :
'N(A^#) = 'N(A).
-
Lemma normalP A B :
reflect (
A \subset B ∧ {in B, normalised A}) (
A <| B).
+
Lemma normalP A B :
reflect (
A \subset B ∧ {in B, normalised A}) (
A <| B).
-
Lemma normal_sub A B :
A <| B → A \subset B.
+
Lemma normal_sub A B :
A <| B → A \subset B.
-
Lemma normal_norm A B :
A <| B → B \subset 'N(A).
+
Lemma normal_norm A B :
A <| B → B \subset 'N(A).
-
Lemma normalS G H K :
K \subset H → H \subset G → K <| G → K <| H.
+
Lemma normalS G H K :
K \subset H → H \subset G → K <| G → K <| H.
-
Lemma normal1 G : 1
<| G.
+
Lemma normal1 G : 1
<| G.
-
Lemma normal_refl G :
G <| G.
+
Lemma normal_refl G :
G <| G.
-
Lemma normalG G :
G <| 'N(G).
+
Lemma normalG G :
G <| 'N(G).
-
Lemma normalSG G H :
H \subset G → H <| 'N_G(H).
+
Lemma normalSG G H :
H \subset G → H <| 'N_G(H).
-
Lemma normalJ A B x :
(A :^ x <| B :^ x) = (A <| B).
+
Lemma normalJ A B x :
(A :^ x <| B :^ x) = (A <| B).
-
Lemma normalM G A B :
A <| G → B <| G → A × B <| G.
+
Lemma normalM G A B :
A <| G → B <| G → A × B <| G.
-
Lemma normalY G A B :
A <| G → B <| G → A <*> B <| G.
+
Lemma normalY G A B :
A <| G → B <| G → A <*> B <| G.
-
Lemma normalYl G H :
(H <| H <*> G) = (G \subset 'N(H)).
+
Lemma normalYl G H :
(H <| H <*> G) = (G \subset 'N(H)).
-
Lemma normalYr G H :
(H <| G <*> H) = (G \subset 'N(H)).
+
Lemma normalYr G H :
(H <| G <*> H) = (G \subset 'N(H)).
-
Lemma normalI G A B :
A <| G → B <| G → A :&: B <| G.
+
Lemma normalI G A B :
A <| G → B <| G → A :&: B <| G.
-
Lemma norm_normalI G A :
G \subset 'N(A) → G :&: A <| G.
+
Lemma norm_normalI G A :
G \subset 'N(A) → G :&: A <| G.
-
Lemma normalGI G H A :
H \subset G → A <| G → H :&: A <| H.
+
Lemma normalGI G H A :
H \subset G → A <| G → H :&: A <| H.
-
Lemma normal_subnorm G H :
(H <| 'N_G(H)) = (H \subset G).
+
Lemma normal_subnorm G H :
(H <| 'N_G(H)) = (H \subset G).
-
Lemma normalD1 A G :
(A^# <| G) = (A <| G).
+
Lemma normalD1 A G :
(A^# <| G) = (A <| G).
-
Lemma gcore_sub A G :
gcore A G \subset A.
+
Lemma gcore_sub A G :
gcore A G \subset A.
-
Lemma gcore_norm A G :
G \subset 'N(gcore A G).
+
Lemma gcore_norm A G :
G \subset 'N(gcore A G).
-
Lemma gcore_normal A G :
A \subset G → gcore A G <| G.
+
Lemma gcore_normal A G :
A \subset G → gcore A G <| G.
-
Lemma gcore_max A B G :
B \subset A → G \subset 'N(B) → B \subset gcore A G.
+
Lemma gcore_max A B G :
B \subset A → G \subset 'N(B) → B \subset gcore A G.
Lemma sub_gcore A B G :
-
G \subset 'N(B) → (B \subset gcore A G) = (B \subset A).
+
G \subset 'N(B) → (B \subset gcore A G) = (B \subset A).
@@ -2781,161 +2750,161 @@
Lemma rcoset_index2 G H x :
-
H \subset G → #|G : H| = 2
→ x \in G :\: H → H :* x = G :\: H.
+
H \subset G → #|G : H| = 2
→ x \in G :\: H → H :* x = G :\: H.
-
Lemma index2_normal G H :
H \subset G → #|G : H| = 2
→ H <| G.
+
Lemma index2_normal G H :
H \subset G → #|G : H| = 2
→ H <| G.
-
Lemma cent1P x y :
reflect (
commute x y) (
x \in 'C[y]).
+
Lemma cent1P x y :
reflect (
commute x y) (
x \in 'C[y]).
-
Lemma cent1id x :
x \in 'C[x].
+
Lemma cent1id x :
x \in 'C[x].
-
Lemma cent1E x y :
(x \in 'C[y]) = (x × y == y × x).
+
Lemma cent1E x y :
(x \in 'C[y]) = (x × y == y × x).
-
Lemma cent1C x y :
(x \in 'C[y]) = (y \in 'C[x]).
+
Lemma cent1C x y :
(x \in 'C[y]) = (y \in 'C[x]).
-
Canonical centraliser_group A :
{group _} :=
Eval hnf in [group of 'C(A)].
+
Canonical centraliser_group A :
{group _} :=
Eval hnf in [group of 'C(A)].
-
Lemma cent_set1 x :
'C([set x]) = 'C[x].
+
Lemma cent_set1 x :
'C([set x]) = 'C[x].
-
Lemma cent1J x y :
'C[x ^ y] = 'C[x] :^ y.
+
Lemma cent1J x y :
'C[x ^ y] = 'C[x] :^ y.
-
Lemma centP A x :
reflect (
centralises x A) (
x \in 'C(A)).
+
Lemma centP A x :
reflect (
centralises x A) (
x \in 'C(A)).
-
Lemma centsP A B :
reflect {in A, centralised B} (
A \subset 'C(B)).
+
Lemma centsP A B :
reflect {in A, centralised B} (
A \subset 'C(B)).
-
Lemma centsC A B :
(A \subset 'C(B)) = (B \subset 'C(A)).
+
Lemma centsC A B :
(A \subset 'C(B)) = (B \subset 'C(A)).
-
Lemma cents1 A :
A \subset 'C(1
).
+
Lemma cents1 A :
A \subset 'C(1
).
-
Lemma cent1T :
'C(1
) = setT :> {set gT}.
+
Lemma cent1T :
'C(1
) = setT :> {set gT}.
-
Lemma cent11T :
'C[1
] = setT :> {set gT}.
+
Lemma cent11T :
'C[1
] = setT :> {set gT}.
-
Lemma cent_sub A :
'C(A) \subset 'N(A).
+
Lemma cent_sub A :
'C(A) \subset 'N(A).
-
Lemma cents_norm A B :
A \subset 'C(B) → A \subset 'N(B).
+
Lemma cents_norm A B :
A \subset 'C(B) → A \subset 'N(B).
-
Lemma centC A B :
A \subset 'C(B) → commute A B.
+
Lemma centC A B :
A \subset 'C(B) → commute A B.
-
Lemma cent_joinEl G H :
G \subset 'C(H) → G <*> H = G × H.
+
Lemma cent_joinEl G H :
G \subset 'C(H) → G <*> H = G × H.
-
Lemma cent_joinEr G H :
H \subset 'C(G) → G <*> H = G × H.
+
Lemma cent_joinEr G H :
H \subset 'C(G) → G <*> H = G × H.
-
Lemma centJ A x :
'C(A :^ x) = 'C(A) :^ x.
+
Lemma centJ A x :
'C(A :^ x) = 'C(A) :^ x.
-
Lemma cent_norm A :
'N(A) \subset 'N('C(A)).
+
Lemma cent_norm A :
'N(A) \subset 'N('C(A)).
-
Lemma norms_cent A B :
A \subset 'N(B) → A \subset 'N('C(B)).
+
Lemma norms_cent A B :
A \subset 'N(B) → A \subset 'N('C(B)).
-
Lemma cent_normal A :
'C(A) <| 'N(A).
+
Lemma cent_normal A :
'C(A) <| 'N(A).
-
Lemma centS A B :
B \subset A → 'C(A) \subset 'C(B).
+
Lemma centS A B :
B \subset A → 'C(A) \subset 'C(B).
-
Lemma centsS A B C :
A \subset B → C \subset 'C(B) → C \subset 'C(A).
+
Lemma centsS A B C :
A \subset B → C \subset 'C(B) → C \subset 'C(A).
Lemma centSS A B C D :
-
A \subset C → B \subset D → C \subset 'C(D) → A \subset 'C(B).
+
A \subset C → B \subset D → C \subset 'C(D) → A \subset 'C(B).
-
Lemma centI A B :
'C(A) <*> 'C(B) \subset 'C(A :&: B).
+
Lemma centI A B :
'C(A) <*> 'C(B) \subset 'C(A :&: B).
-
Lemma centU A B :
'C(A :|: B) = 'C(A) :&: 'C(B).
+
Lemma centU A B :
'C(A :|: B) = 'C(A) :&: 'C(B).
-
Lemma cent_gen A :
'C(<<A>>) = 'C(A).
+
Lemma cent_gen A :
'C(<<A>>) = 'C(A).
-
Lemma cent_cycle x :
'C(<[x]>) = 'C[x].
+
Lemma cent_cycle x :
'C(<[x]>) = 'C[x].
-
Lemma sub_cent1 A x :
(A \subset 'C[x]) = (x \in 'C(A)).
+
Lemma sub_cent1 A x :
(A \subset 'C[x]) = (x \in 'C(A)).
-
Lemma cents_cycle x y :
commute x y → <[x]> \subset 'C(<[y]>).
+
Lemma cents_cycle x y :
commute x y → <[x]> \subset 'C(<[y]>).
-
Lemma cycle_abelian x :
abelian <[x]>.
+
Lemma cycle_abelian x :
abelian <[x]>.
-
Lemma centY A B :
'C(A <*> B) = 'C(A) :&: 'C(B).
+
Lemma centY A B :
'C(A <*> B) = 'C(A) :&: 'C(B).
-
Lemma centM G H :
'C(G × H) = 'C(G) :&: 'C(H).
+
Lemma centM G H :
'C(G × H) = 'C(G) :&: 'C(H).
-
Lemma cent_classP x G :
reflect (
x ^: G = [set x]) (
x \in 'C(G)).
+
Lemma cent_classP x G :
reflect (
x ^: G = [set x]) (
x \in 'C(G)).
-
Lemma commG1P A B :
reflect (
[~: A, B] = 1) (
A \subset 'C(B)).
+
Lemma commG1P A B :
reflect (
[~: A, B] = 1) (
A \subset 'C(B)).
-
Lemma abelianE A :
abelian A = (A \subset 'C(A)).
+
Lemma abelianE A :
abelian A = (A \subset 'C(A)).
-
Lemma abelian1 :
abelian [1 gT].
+
Lemma abelian1 :
abelian [1 gT].
-
Lemma abelianS A B :
A \subset B → abelian B → abelian A.
+
Lemma abelianS A B :
A \subset B → abelian B → abelian A.
-
Lemma abelianJ A x :
abelian (
A :^ x)
= abelian A.
+
Lemma abelianJ A x :
abelian (
A :^ x)
= abelian A.
-
Lemma abelian_gen A :
abelian <<A>> = abelian A.
+
Lemma abelian_gen A :
abelian <<A>> = abelian A.
Lemma abelianY A B :
-
abelian (
A <*> B)
= [&& abelian A, abelian B & B \subset 'C(A)].
+
abelian (
A <*> B)
= [&& abelian A, abelian B & B \subset 'C(A)].
Lemma abelianM G H :
-
abelian (
G × H)
= [&& abelian G, abelian H & H \subset 'C(G)].
+
abelian (
G × H)
= [&& abelian G, abelian H & H \subset 'C(G)].
Section SubAbelian.
-
Variable A B C :
{set gT}.
+
Variable A B C :
{set gT}.
Hypothesis cAA :
abelian A.
-
Lemma sub_abelian_cent :
C \subset A → A \subset 'C(C).
+
Lemma sub_abelian_cent :
C \subset A → A \subset 'C(C).
-
Lemma sub_abelian_cent2 :
B \subset A → C \subset A → B \subset 'C(C).
+
Lemma sub_abelian_cent2 :
B \subset A → C \subset A → B \subset 'C(C).
-
Lemma sub_abelian_norm :
C \subset A → A \subset 'N(C).
+
Lemma sub_abelian_norm :
C \subset A → A \subset 'N(C).
-
Lemma sub_abelian_normal :
(C \subset A) = (C <| A).
+
Lemma sub_abelian_normal :
(C \subset A) = (C <| A).
End SubAbelian.
@@ -2948,83 +2917,85 @@
-
-
-
Notation "''N' ( A )" := (
normaliser_group A) :
Group_scope.
-
Notation "''C' ( A )" := (
centraliser_group A) :
Group_scope.
-
Notation "''C' [ x ]" := (
normaliser_group [set x%
g]) :
Group_scope.
-
Notation "''N_' G ( A )" := (
setI_group G 'N(A)) :
Group_scope.
-
Notation "''C_' G ( A )" := (
setI_group G 'C(A)) :
Group_scope.
-
Notation "''C_' ( G ) ( A )" := (
setI_group G 'C(A))
+
Notation "''N' ( A )" := (
normaliser_group A) :
Group_scope.
+
Notation "''C' ( A )" := (
centraliser_group A) :
Group_scope.
+
Notation "''C' [ x ]" := (
normaliser_group [set x%
g]) :
Group_scope.
+
Notation "''N_' G ( A )" := (
setI_group G 'N(A)) :
Group_scope.
+
Notation "''C_' G ( A )" := (
setI_group G 'C(A)) :
Group_scope.
+
Notation "''C_' ( G ) ( A )" := (
setI_group G 'C(A))
(
only parsing) :
Group_scope.
-
Notation "''C_' G [ x ]" := (
setI_group G 'C[x]) :
Group_scope.
-
Notation "''C_' ( G ) [ x ]" := (
setI_group G 'C[x])
+
Notation "''C_' G [ x ]" := (
setI_group G 'C[x]) :
Group_scope.
+
Notation "''C_' ( G ) [ x ]" := (
setI_group G 'C[x])
(
only parsing) :
Group_scope.
-
Hint Resolve normG normal_refl.
+
Hint Extern 0 (
is_true (
_ \subset _)) ⇒
apply:
normG :
core.
+
Hint Extern 0 (
is_true (
_ <| _)) ⇒
apply:
normal_refl :
core.
Section MinMaxGroup.
Variable gT :
finGroupType.
-
Variable gP :
pred {group gT}.
+
Implicit Types gP :
pred {group gT}.
+
+
+
Definition maxgroup A gP :=
maxset (
fun A ⇒
group_set A && gP <<A>>%
G)
A.
+
Definition mingroup A gP :=
minset (
fun A ⇒
group_set A && gP <<A>>%
G)
A.
-
Definition maxgroup :=
maxset (
fun A ⇒
group_set A && gP <<A>>).
-
Definition mingroup :=
minset (
fun A ⇒
group_set A && gP <<A>>).
+
Variable gP :
pred {group gT}.
-
Lemma ex_maxgroup :
(∃ G, gP G) → {G : {group gT} | maxgroup G}.
+
Lemma ex_maxgroup :
(∃ G, gP G) → {G : {group gT} | maxgroup G gP}.
-
Lemma ex_mingroup :
(∃ G, gP G) → {G : {group gT} | mingroup G}.
+
Lemma ex_mingroup :
(∃ G, gP G) → {G : {group gT} | mingroup G gP}.
-
Variable G :
{group gT}.
+
Variable G :
{group gT}.
Lemma mingroupP :
-
reflect (
gP G ∧ ∀ H,
gP H → H \subset G → H :=: G) (
mingroup G).
+
reflect (
gP G ∧ ∀ H,
gP H → H \subset G → H :=: G) (
mingroup G gP).
Lemma maxgroupP :
-
reflect (
gP G ∧ ∀ H,
gP H → G \subset H → H :=: G) (
maxgroup G).
+
reflect (
gP G ∧ ∀ H,
gP H → G \subset H → H :=: G) (
maxgroup G gP).
-
Lemma maxgroupp :
maxgroup G → gP G.
+
Lemma maxgroupp :
maxgroup G gP → gP G.
-
Lemma mingroupp :
mingroup G → gP G.
+
Lemma mingroupp :
mingroup G gP → gP G.
Hypothesis gPG :
gP G.
-
Lemma maxgroup_exists :
{H : {group gT} | maxgroup H & G \subset H}.
+
Lemma maxgroup_exists :
{H : {group gT} | maxgroup H gP & G \subset H}.
-
Lemma mingroup_exists :
{H : {group gT} | mingroup H & H \subset G}.
+
Lemma mingroup_exists :
{H : {group gT} | mingroup H gP & H \subset G}.
End MinMaxGroup.
-
Notation "[ 'max' A 'of' G | gP ]" :=
- (
maxgroup (
fun G :
{group _} ⇒
gP)
A) :
group_scope.
-
Notation "[ 'max' G | gP ]" :=
[max gval G of G | gP] :
group_scope.
-
Notation "[ 'max' A 'of' G | gP & gQ ]" :=
-
[max A of G | gP && gQ] :
group_scope.
-
Notation "[ 'max' G | gP & gQ ]" :=
[max G | gP && gQ] :
group_scope.
-
Notation "[ 'min' A 'of' G | gP ]" :=
- (
mingroup (
fun G :
{group _} ⇒
gP)
A) :
group_scope.
-
Notation "[ 'min' G | gP ]" :=
[min gval G of G | gP] :
group_scope.
-
Notation "[ 'min' A 'of' G | gP & gQ ]" :=
-
[min A of G | gP && gQ] :
group_scope.
-
Notation "[ 'min' G | gP & gQ ]" :=
[min G | gP && gQ] :
group_scope.
+
Notation "[ 'max' A 'of' G | gP ]" :=
+ (
maxgroup A (
fun G :
{group _} ⇒
gP)) :
group_scope.
+
Notation "[ 'max' G | gP ]" :=
[max gval G of G | gP] :
group_scope.
+
Notation "[ 'max' A 'of' G | gP & gQ ]" :=
+
[max A of G | gP && gQ] :
group_scope.
+
Notation "[ 'max' G | gP & gQ ]" :=
[max G | gP && gQ] :
group_scope.
+
Notation "[ 'min' A 'of' G | gP ]" :=
+ (
mingroup A (
fun G :
{group _} ⇒
gP)) :
group_scope.
+
Notation "[ 'min' G | gP ]" :=
[min gval G of G | gP] :
group_scope.
+
Notation "[ 'min' A 'of' G | gP & gQ ]" :=
+
[min A of G | gP && gQ] :
group_scope.
+
Notation "[ 'min' G | gP & gQ ]" :=
[min G | gP && gQ] :
group_scope.
--
cgit v1.2.3