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.solvable.nilpotent.html | 295 +++++++++++++-------------
1 file changed, 147 insertions(+), 148 deletions(-)
(limited to 'docs/htmldoc/mathcomp.solvable.nilpotent.html')
diff --git a/docs/htmldoc/mathcomp.solvable.nilpotent.html b/docs/htmldoc/mathcomp.solvable.nilpotent.html
index 7aeb0e8..dbee59d 100644
--- a/docs/htmldoc/mathcomp.solvable.nilpotent.html
+++ b/docs/htmldoc/mathcomp.solvable.nilpotent.html
@@ -21,7 +21,6 @@
@@ -57,13 +56,13 @@
Section SeriesDefs.
-Variables (n : nat) (gT : finGroupType) (A : {set gT}).
+Variables (n : nat) (gT : finGroupType) (A : {set gT}).
-Definition lower_central_at_rec := iter n (fun B ⇒ [~: B, A]) A.
+Definition lower_central_at_rec := iter n (fun B ⇒ [~: B, A]) A.
-Definition upper_central_at_rec := iter n (fun B ⇒ coset B @*^-1 'Z(A / B)) 1.
+Definition upper_central_at_rec := iter n (fun B ⇒ coset B @*^-1 'Z(A / B)) 1.
End SeriesDefs.
@@ -76,7 +75,7 @@
starts at 0 (sic).
@@ -86,34 +85,34 @@
"cooking" destroys it.
-
Definition upper_central_at :=
nosimpl upper_central_at_rec.
+
Definition upper_central_at :=
nosimpl upper_central_at_rec.
-
Notation "''L_' n ( G )" := (
lower_central_at n G)
+
Notation "''L_' n ( G )" := (
lower_central_at n G)
(
at level 8,
n at level 2,
format "''L_' n ( G )") :
group_scope.
-
Notation "''Z_' n ( G )" := (
upper_central_at n G)
+
Notation "''Z_' n ( G )" := (
upper_central_at n G)
(
at level 8,
n at level 2,
format "''Z_' n ( G )") :
group_scope.
Section PropertiesDefs.
-
Variables (
gT :
finGroupType) (
A :
{set gT}).
+
Variables (
gT :
finGroupType) (
A :
{set gT}).
Definition nilpotent :=
-
[∀ (G : {group gT} | G \subset A :&: [~: G, A]), G :==: 1
].
+
[∀ (G : {group gT} | G \subset A :&: [~: G, A]), G :==: 1
].
-
Definition nil_class :=
index 1 (
mkseq (
fun n ⇒
'L_n.+1(A))
#|A|).
+
Definition nil_class :=
index 1 (
mkseq (
fun n ⇒
'L_n.+1(A))
#|A|).
Definition solvable :=
-
[∀ (G : {group gT} | G \subset A :&: [~: G, G]), G :==: 1
].
+
[∀ (G : {group gT} | G \subset A :&: [~: G, G]), G :==: 1
].
End PropertiesDefs.
@@ -125,27 +124,27 @@
Variable gT:
finGroupType.
-
Implicit Types (
A B :
{set gT}) (
G H :
{group gT}).
+
Implicit Types (
A B :
{set gT}) (
G H :
{group gT}).
-
Lemma nilpotent1 :
nilpotent [1 gT].
+
Lemma nilpotent1 :
nilpotent [1 gT].
-
Lemma nilpotentS A B :
B \subset A → nilpotent A → nilpotent B.
+
Lemma nilpotentS A B :
B \subset A → nilpotent A → nilpotent B.
Lemma nil_comm_properl G H A :
-
nilpotent G → H \subset G → H :!=: 1
→ A \subset 'N_G(H) →
-
[~: H, A] \proper H.
+
nilpotent G → H \subset G → H :!=: 1
→ A \subset 'N_G(H) →
+
[~: H, A] \proper H.
Lemma nil_comm_properr G A H :
-
nilpotent G → H \subset G → H :!=: 1
→ A \subset 'N_G(H) →
-
[~: A, H] \proper H.
+
nilpotent G → H \subset G → H :!=: 1
→ A \subset 'N_G(H) →
+
[~: A, H] \proper H.
-
Lemma centrals_nil (
s :
seq {group gT})
G :
-
G.-central.-series 1%
G s → last 1%
G s = G → nilpotent G.
+
Lemma centrals_nil (
s :
seq {group gT})
G :
+
G.-central.-series 1%
G s → last 1%
G s = G → nilpotent G.
End NilpotentProps.
@@ -155,138 +154,138 @@
Variable gT :
finGroupType.
-
Implicit Types (
A B :
{set gT}) (
G H :
{group gT}).
+
Implicit Types (
A B :
{set gT}) (
G H :
{group gT}).
-
Lemma lcn0 A :
'L_0(A) = A.
-
Lemma lcn1 A :
'L_1(A) = A.
-
Lemma lcnSn n A :
'L_n.+2(A) = [~: 'L_n.+1(A), A].
-
Lemma lcnSnS n G :
[~: 'L_n(G), G] \subset 'L_n.+1(G).
-
Lemma lcnE n A :
'L_n.+1(A) = lower_central_at_rec n A.
-
Lemma lcn2 A :
'L_2(A) = A^`(1
).
+
Lemma lcn0 A :
'L_0(A) = A.
+
Lemma lcn1 A :
'L_1(A) = A.
+
Lemma lcnSn n A :
'L_n.+2(A) = [~: 'L_n.+1(A), A].
+
Lemma lcnSnS n G :
[~: 'L_n(G), G] \subset 'L_n.+1(G).
+
Lemma lcnE n A :
'L_n.+1(A) = lower_central_at_rec n A.
+
Lemma lcn2 A :
'L_2(A) = A^`(1
).
-
Lemma lcn_group_set n G :
group_set 'L_n(G).
+
Lemma lcn_group_set n G :
group_set 'L_n(G).
Canonical lower_central_at_group n G :=
Group (
lcn_group_set n G).
-
Lemma lcn_char n G :
'L_n(G) \char G.
+
Lemma lcn_char n G :
'L_n(G) \char G.
-
Lemma lcn_normal n G :
'L_n(G) <| G.
+
Lemma lcn_normal n G :
'L_n(G) <| G.
-
Lemma lcn_sub n G :
'L_n(G) \subset G.
+
Lemma lcn_sub n G :
'L_n(G) \subset G.
-
Lemma lcn_norm n G :
G \subset 'N('L_n(G)).
+
Lemma lcn_norm n G :
G \subset 'N('L_n(G)).
-
Lemma lcn_subS n G :
'L_n.+1(G) \subset 'L_n(G).
+
Lemma lcn_subS n G :
'L_n.+1(G) \subset 'L_n(G).
-
Lemma lcn_normalS n G :
'L_n.+1(G) <| 'L_n(G).
+
Lemma lcn_normalS n G :
'L_n.+1(G) <| 'L_n(G).
-
Lemma lcn_central n G :
'L_n(G) / 'L_n.+1(G) \subset 'Z(G / 'L_n.+1(G)).
+
Lemma lcn_central n G :
'L_n(G) / 'L_n.+1(G) \subset 'Z(G / 'L_n.+1(G)).
-
Lemma lcn_sub_leq m n G :
n ≤ m → 'L_m(G) \subset 'L_n(G).
+
Lemma lcn_sub_leq m n G :
n ≤ m → 'L_m(G) \subset 'L_n(G).
-
Lemma lcnS n A B :
A \subset B → 'L_n(A) \subset 'L_n(B).
+
Lemma lcnS n A B :
A \subset B → 'L_n(A) \subset 'L_n(B).
-
Lemma lcn_cprod n A B G :
A \* B = G → 'L_n(A) \* 'L_n(B) = 'L_n(G).
+
Lemma lcn_cprod n A B G :
A \* B = G → 'L_n(A) \* 'L_n(B) = 'L_n(G).
-
Lemma lcn_dprod n A B G :
A \x B = G → 'L_n(A) \x 'L_n(B) = 'L_n(G).
+
Lemma lcn_dprod n A B G :
A \x B = G → 'L_n(A) \x 'L_n(B) = 'L_n(G).
-
Lemma der_cprod n A B G :
A \* B = G → A^`(n) \* B^`(n) = G^`(n).
+
Lemma der_cprod n A B G :
A \* B = G → A^`(n) \* B^`(n) = G^`(n).
-
Lemma der_dprod n A B G :
A \x B = G → A^`(n) \x B^`(n) = G^`(n).
+
Lemma der_dprod n A B G :
A \x B = G → A^`(n) \x B^`(n) = G^`(n).
-
Lemma lcn_bigcprod n I r P (
F :
I → {set gT})
G :
-
\big[cprod/1
]_(i <- r | P i) F i = G →
-
\big[cprod/1
]_(i <- r | P i) 'L_n(F i) = 'L_n(G).
+
Lemma lcn_bigcprod n I r P (
F :
I → {set gT})
G :
+
\big[cprod/1
]_(i <- r | P i) F i = G →
+
\big[cprod/1
]_(i <- r | P i) 'L_n(F i) = 'L_n(G).
-
Lemma lcn_bigdprod n I r P (
F :
I → {set gT})
G :
-
\big[dprod/1
]_(i <- r | P i) F i = G →
-
\big[dprod/1
]_(i <- r | P i) 'L_n(F i) = 'L_n(G).
+
Lemma lcn_bigdprod n I r P (
F :
I → {set gT})
G :
+
\big[dprod/1
]_(i <- r | P i) F i = G →
+
\big[dprod/1
]_(i <- r | P i) 'L_n(F i) = 'L_n(G).
-
Lemma der_bigcprod n I r P (
F :
I → {set gT})
G :
-
\big[cprod/1
]_(i <- r | P i) F i = G →
-
\big[cprod/1
]_(i <- r | P i) (F i)^`(n) = G^`(n).
+
Lemma der_bigcprod n I r P (
F :
I → {set gT})
G :
+
\big[cprod/1
]_(i <- r | P i) F i = G →
+
\big[cprod/1
]_(i <- r | P i) (F i)^`(n) = G^`(n).
-
Lemma der_bigdprod n I r P (
F :
I → {set gT})
G :
-
\big[dprod/1
]_(i <- r | P i) F i = G →
-
\big[dprod/1
]_(i <- r | P i) (F i)^`(n) = G^`(n).
+
Lemma der_bigdprod n I r P (
F :
I → {set gT})
G :
+
\big[dprod/1
]_(i <- r | P i) F i = G →
+
\big[dprod/1
]_(i <- r | P i) (F i)^`(n) = G^`(n).
-
Lemma nilpotent_class G :
nilpotent G = (nil_class G < #|G|).
+
Lemma nilpotent_class G :
nilpotent G = (nil_class G < #|G|).
Lemma lcn_nil_classP n G :
-
nilpotent G → reflect (
'L_n.+1(G) = 1) (
nil_class G ≤ n).
+
nilpotent G → reflect (
'L_n.+1(G) = 1) (
nil_class G ≤ n).
-
Lemma lcnP G :
reflect (
∃ n, 'L_n.+1(G) = 1) (
nilpotent G).
+
Lemma lcnP G :
reflect (
∃ n, 'L_n.+1(G) = 1) (
nilpotent G).
-
Lemma abelian_nil G :
abelian G → nilpotent G.
+
Lemma abelian_nil G :
abelian G → nilpotent G.
-
Lemma nil_class0 G :
(nil_class G == 0
) = (G :==: 1
).
+
Lemma nil_class0 G :
(nil_class G == 0
) = (G :==: 1
).
-
Lemma nil_class1 G :
(nil_class G ≤ 1
) = abelian G.
+
Lemma nil_class1 G :
(nil_class G ≤ 1
) = abelian G.
-
Lemma cprod_nil A B G :
A \* B = G → nilpotent G = nilpotent A && nilpotent B.
+
Lemma cprod_nil A B G :
A \* B = G → nilpotent G = nilpotent A && nilpotent B.
Lemma mulg_nil G H :
-
H \subset 'C(G) → nilpotent (
G × H)
= nilpotent G && nilpotent H.
+
H \subset 'C(G) → nilpotent (
G × H)
= nilpotent G && nilpotent H.
-
Lemma dprod_nil A B G :
A \x B = G → nilpotent G = nilpotent A && nilpotent B.
+
Lemma dprod_nil A B G :
A \x B = G → nilpotent G = nilpotent A && nilpotent B.
-
Lemma bigdprod_nil I r (
P :
pred I) (
A_ :
I → {set gT})
G :
-
\big[dprod/1
]_(i <- r | P i) A_ i = G
-
→ (∀ i,
P i → nilpotent (
A_ i)
) → nilpotent G.
+
Lemma bigdprod_nil I r (
P :
pred I) (
A_ :
I → {set gT})
G :
+
\big[dprod/1
]_(i <- r | P i) A_ i = G
+
→ (∀ i,
P i → nilpotent (
A_ i)
) → nilpotent G.
End LowerCentral.
-
Notation "''L_' n ( G )" := (
lower_central_at_group n G) :
Group_scope.
+
Notation "''L_' n ( G )" := (
lower_central_at_group n G) :
Group_scope.
-
Lemma lcn_cont n :
GFunctor.continuous (
lower_central_at n).
+
Lemma lcn_cont n :
GFunctor.continuous (@
lower_central_at n).
-
Canonical lcn_igFun n :=
[igFun by lcn_sub^~ n & lcn_cont n].
-
Canonical lcn_gFun n :=
[gFun by lcn_cont n].
-
Canonical lcn_mgFun n :=
[mgFun by fun _ G H ⇒ @
lcnS _ n G H].
+
Canonical lcn_igFun n :=
[igFun by lcn_sub^~ n & lcn_cont n].
+
Canonical lcn_gFun n :=
[gFun by lcn_cont n].
+
Canonical lcn_mgFun n :=
[mgFun by fun _ G H ⇒ @
lcnS _ n G H].
Section UpperCentralFunctor.
-
Variable n :
nat.
+
Variable n :
nat.
Implicit Type gT :
finGroupType.
-
Lemma ucn_pmap :
∃ hZ :
GFunctor.pmap, @
upper_central_at n = hZ.
+
Lemma ucn_pmap :
∃ hZ :
GFunctor.pmap, @
upper_central_at n = hZ.
-
Lemma ucn_group_set gT (
G :
{group gT}) :
group_set 'Z_n(G).
+
Lemma ucn_group_set gT (
G :
{group gT}) :
group_set 'Z_n(G).
Canonical upper_central_at_group gT G :=
Group (@
ucn_group_set gT G).
-
Lemma ucn_sub gT (
G :
{group gT}) :
'Z_n(G) \subset G.
+
Lemma ucn_sub gT (
G :
{group gT}) :
'Z_n(G) \subset G.
-
Lemma morphim_ucn :
GFunctor.pcontinuous (
upper_central_at n).
+
Lemma morphim_ucn :
GFunctor.pcontinuous (@
upper_central_at n).
-
Canonical ucn_igFun :=
[igFun by ucn_sub & morphim_ucn].
-
Canonical ucn_gFun :=
[gFun by morphim_ucn].
-
Canonical ucn_pgFun :=
[pgFun by morphim_ucn].
+
Canonical ucn_igFun :=
[igFun by ucn_sub & morphim_ucn].
+
Canonical ucn_gFun :=
[gFun by morphim_ucn].
+
Canonical ucn_pgFun :=
[pgFun by morphim_ucn].
-
Variable (
gT :
finGroupType) (
G :
{group gT}).
+
Variable (
gT :
finGroupType) (
G :
{group gT}).
-
Lemma ucn_char :
'Z_n(G) \char G.
-
Lemma ucn_norm :
G \subset 'N('Z_n(G)).
-
Lemma ucn_normal :
'Z_n(G) <| G.
+
Lemma ucn_char :
'Z_n(G) \char G.
+
Lemma ucn_norm :
G \subset 'N('Z_n(G)).
+
Lemma ucn_normal :
'Z_n(G) <| G.
End UpperCentralFunctor.
-
Notation "''Z_' n ( G )" := (
upper_central_at_group n G) :
Group_scope.
+
Notation "''Z_' n ( G )" := (
upper_central_at_group n G) :
Group_scope.
Section UpperCentral.
Variable gT :
finGroupType.
-
Implicit Types (
A B :
{set gT}) (
G H :
{group gT}).
+
Implicit Types (
A B :
{set gT}) (
G H :
{group gT}).
-
Lemma ucn0 A :
'Z_0(A) = 1.
+
Lemma ucn0 A :
'Z_0(A) = 1.
-
Lemma ucnSn n A :
'Z_n.+1(A) = coset 'Z_n(A) @*^-1 'Z(A / 'Z_n(A)).
+
Lemma ucnSn n A :
'Z_n.+1(A) = coset 'Z_n(A) @*^-1 'Z(A / 'Z_n(A)).
-
Lemma ucnE n A :
'Z_n(A) = upper_central_at_rec n A.
+
Lemma ucnE n A :
'Z_n(A) = upper_central_at_rec n A.
-
Lemma ucn_subS n G :
'Z_n(G) \subset 'Z_n.+1(G).
+
Lemma ucn_subS n G :
'Z_n(G) \subset 'Z_n.+1(G).
-
Lemma ucn_sub_geq m n G :
n ≥ m → 'Z_m(G) \subset 'Z_n(G).
+
Lemma ucn_sub_geq m n G :
n ≥ m → 'Z_m(G) \subset 'Z_n(G).
-
Lemma ucn_central n G :
'Z_n.+1(G) / 'Z_n(G) = 'Z(G / 'Z_n(G)).
+
Lemma ucn_central n G :
'Z_n.+1(G) / 'Z_n(G) = 'Z(G / 'Z_n(G)).
-
Lemma ucn_normalS n G :
'Z_n(G) <| 'Z_n.+1(G).
+
Lemma ucn_normalS n G :
'Z_n(G) <| 'Z_n.+1(G).
-
Lemma ucn_comm n G :
[~: 'Z_n.+1(G), G] \subset 'Z_n(G).
+
Lemma ucn_comm n G :
[~: 'Z_n.+1(G), G] \subset 'Z_n(G).
-
Lemma ucn1 G :
'Z_1(G) = 'Z(G).
+
Lemma ucn1 G :
'Z_1(G) = 'Z(G).
-
Lemma ucnSnR n G :
'Z_n.+1(G) = [set x in G | [~: [set x], G] \subset 'Z_n(G)].
+
Lemma ucnSnR n G :
'Z_n.+1(G) = [set x in G | [~: [set x], G] \subset 'Z_n(G)].
-
Lemma ucn_cprod n A B G :
A \* B = G → 'Z_n(A) \* 'Z_n(B) = 'Z_n(G).
+
Lemma ucn_cprod n A B G :
A \* B = G → 'Z_n(A) \* 'Z_n(B) = 'Z_n(G).
-
Lemma ucn_dprod n A B G :
A \x B = G → 'Z_n(A) \x 'Z_n(B) = 'Z_n(G).
+
Lemma ucn_dprod n A B G :
A \x B = G → 'Z_n(A) \x 'Z_n(B) = 'Z_n(G).
-
Lemma ucn_bigcprod n I r P (
F :
I → {set gT})
G :
-
\big[cprod/1
]_(i <- r | P i) F i = G →
-
\big[cprod/1
]_(i <- r | P i) 'Z_n(F i) = 'Z_n(G).
+
Lemma ucn_bigcprod n I r P (
F :
I → {set gT})
G :
+
\big[cprod/1
]_(i <- r | P i) F i = G →
+
\big[cprod/1
]_(i <- r | P i) 'Z_n(F i) = 'Z_n(G).
-
Lemma ucn_bigdprod n I r P (
F :
I → {set gT})
G :
-
\big[dprod/1
]_(i <- r | P i) F i = G →
-
\big[dprod/1
]_(i <- r | P i) 'Z_n(F i) = 'Z_n(G).
+
Lemma ucn_bigdprod n I r P (
F :
I → {set gT})
G :
+
\big[dprod/1
]_(i <- r | P i) F i = G →
+
\big[dprod/1
]_(i <- r | P i) 'Z_n(F i) = 'Z_n(G).
-
Lemma ucn_lcnP n G :
('L_n.+1(G) == 1
) = ('Z_n(G) == G).
+
Lemma ucn_lcnP n G :
('L_n.+1(G) == 1
) = ('Z_n(G) == G).
-
Lemma ucnP G :
reflect (
∃ n, 'Z_n(G) = G) (
nilpotent G).
+
Lemma ucnP G :
reflect (
∃ n, 'Z_n(G) = G) (
nilpotent G).
Lemma ucn_nil_classP n G :
-
nilpotent G → reflect (
'Z_n(G) = G) (
nil_class G ≤ n).
+
nilpotent G → reflect (
'Z_n(G) = G) (
nil_class G ≤ n).
-
Lemma ucn_id n G :
'Z_n('Z_n(G)) = 'Z_n(G).
+
Lemma ucn_id n G :
'Z_n('Z_n(G)) = 'Z_n(G).
-
Lemma ucn_nilpotent n G :
nilpotent 'Z_n(G).
+
Lemma ucn_nilpotent n G :
nilpotent 'Z_n(G).
-
Lemma nil_class_ucn n G :
nil_class 'Z_n(G) ≤ n.
+
Lemma nil_class_ucn n G :
nil_class 'Z_n(G) ≤ n.
End UpperCentral.
@@ -406,27 +405,27 @@
Section MorphNil.
-
Variables (
aT rT :
finGroupType) (
D :
{group aT}) (
f :
{morphism D >-> rT}).
-
Implicit Type G :
{group aT}.
+
Variables (
aT rT :
finGroupType) (
D :
{group aT}) (
f :
{morphism D >-> rT}).
+
Implicit Type G :
{group aT}.
-
Lemma morphim_lcn n G :
G \subset D → f @* 'L_n(G) = 'L_n(f @* G).
+
Lemma morphim_lcn n G :
G \subset D → f @* 'L_n(G) = 'L_n(f @* G).
-
Lemma injm_ucn n G :
'injm f → G \subset D → f @* 'Z_n(G) = 'Z_n(f @* G).
+
Lemma injm_ucn n G :
'injm f → G \subset D → f @* 'Z_n(G) = 'Z_n(f @* G).
-
Lemma morphim_nil G :
nilpotent G → nilpotent (
f @* G).
+
Lemma morphim_nil G :
nilpotent G → nilpotent (
f @* G).
-
Lemma injm_nil G :
'injm f → G \subset D → nilpotent (
f @* G)
= nilpotent G.
+
Lemma injm_nil G :
'injm f → G \subset D → nilpotent (
f @* G)
= nilpotent G.
-
Lemma nil_class_morphim G :
nilpotent G → nil_class (
f @* G)
≤ nil_class G.
+
Lemma nil_class_morphim G :
nilpotent G → nil_class (
f @* G)
≤ nil_class G.
Lemma nil_class_injm G :
-
'injm f → G \subset D → nil_class (
f @* G)
= nil_class G.
+
'injm f → G \subset D → nil_class (
f @* G)
= nil_class G.
End MorphNil.
@@ -436,52 +435,52 @@
Variables gT :
finGroupType.
-
Implicit Types (
rT :
finGroupType) (
G H :
{group gT}).
+
Implicit Types (
rT :
finGroupType) (
G H :
{group gT}).
-
Lemma quotient_ucn_add m n G :
'Z_(m + n)(G) / 'Z_n(G) = 'Z_m(G / 'Z_n(G)).
+
Lemma quotient_ucn_add m n G :
'Z_(m + n)(G) / 'Z_n(G) = 'Z_m(G / 'Z_n(G)).
-
Lemma isog_nil rT G (
L :
{group rT}) :
G \isog L → nilpotent G = nilpotent L.
+
Lemma isog_nil rT G (
L :
{group rT}) :
G \isog L → nilpotent G = nilpotent L.
-
Lemma isog_nil_class rT G (
L :
{group rT}) :
-
G \isog L → nil_class G = nil_class L.
+
Lemma isog_nil_class rT G (
L :
{group rT}) :
+
G \isog L → nil_class G = nil_class L.
-
Lemma quotient_nil G H :
nilpotent G → nilpotent (
G / H).
+
Lemma quotient_nil G H :
nilpotent G → nilpotent (
G / H).
-
Lemma quotient_center_nil G :
nilpotent (
G / 'Z(G))
= nilpotent G.
+
Lemma quotient_center_nil G :
nilpotent (
G / 'Z(G))
= nilpotent G.
Lemma nil_class_quotient_center G :
-
nilpotent (
G)
→ nil_class (
G / 'Z(G))
= (nil_class G).-1.
+
nilpotent (
G)
→ nil_class (
G / 'Z(G))
= (nil_class G).-1.
Lemma nilpotent_sub_norm G H :
-
nilpotent G → H \subset G → 'N_G(H) \subset H → G :=: H.
+
nilpotent G → H \subset G → 'N_G(H) \subset H → G :=: H.
Lemma nilpotent_proper_norm G H :
-
nilpotent G → H \proper G → H \proper 'N_G(H).
+
nilpotent G → H \proper G → H \proper 'N_G(H).
-
Lemma nilpotent_subnormal G H :
nilpotent G → H \subset G → H <|<| G.
+
Lemma nilpotent_subnormal G H :
nilpotent G → H \subset G → H <|<| G.
-
Lemma TI_center_nil G H :
nilpotent G → H <| G → H :&: 'Z(G) = 1
→ H :=: 1.
+
Lemma TI_center_nil G H :
nilpotent G → H <| G → H :&: 'Z(G) = 1
→ H :=: 1.
Lemma meet_center_nil G H :
-
nilpotent G → H <| G → H :!=: 1
→ H :&: 'Z(G) != 1.
+
nilpotent G → H <| G → H :!=: 1
→ H :&: 'Z(G) != 1.
-
Lemma center_nil_eq1 G :
nilpotent G → ('Z(G) == 1
) = (G :==: 1
).
+
Lemma center_nil_eq1 G :
nilpotent G → ('Z(G) == 1
) = (G :==: 1
).
Lemma cyclic_nilpotent_quo_der1_cyclic G :
-
nilpotent G → cyclic (
G / G^`(1
))
→ cyclic G.
+
nilpotent G → cyclic (
G / G^`(1
))
→ cyclic G.
End QuotientNil.
@@ -491,26 +490,26 @@
Variable gT :
finGroupType.
-
Implicit Types G H :
{group gT}.
+
Implicit Types G H :
{group gT}.
-
Lemma nilpotent_sol G :
nilpotent G → solvable G.
+
Lemma nilpotent_sol G :
nilpotent G → solvable G.
-
Lemma abelian_sol G :
abelian G → solvable G.
+
Lemma abelian_sol G :
abelian G → solvable G.
-
Lemma solvable1 :
solvable [1 gT].
+
Lemma solvable1 :
solvable [1 gT].
-
Lemma solvableS G H :
H \subset G → solvable G → solvable H.
+
Lemma solvableS G H :
H \subset G → solvable G → solvable H.
Lemma sol_der1_proper G H :
-
solvable G → H \subset G → H :!=: 1
→ H^`(1
) \proper H.
+
solvable G → H \subset G → H :!=: 1
→ H^`(1
) \proper H.
-
Lemma derivedP G :
reflect (
∃ n, G^`(n) = 1) (
solvable G).
+
Lemma derivedP G :
reflect (
∃ n, G^`(n) = 1) (
solvable G).
End Solvable.
@@ -519,14 +518,14 @@
Section MorphSol.
-
Variables (
gT rT :
finGroupType) (
D :
{group gT}) (
f :
{morphism D >-> rT}).
-
Variable G :
{group gT}.
+
Variables (
gT rT :
finGroupType) (
D :
{group gT}) (
f :
{morphism D >-> rT}).
+
Variable G :
{group gT}.
-
Lemma morphim_sol :
solvable G → solvable (
f @* G).
+
Lemma morphim_sol :
solvable G → solvable (
f @* G).
-
Lemma injm_sol :
'injm f → G \subset D → solvable (
f @* G)
= solvable G.
+
Lemma injm_sol :
'injm f → G \subset D → solvable (
f @* G)
= solvable G.
End MorphSol.
@@ -536,19 +535,19 @@
Variables gT rT :
finGroupType.
-
Implicit Types G H K :
{group gT}.
+
Implicit Types G H K :
{group gT}.
-
Lemma isog_sol G (
L :
{group rT}) :
G \isog L → solvable G = solvable L.
+
Lemma isog_sol G (
L :
{group rT}) :
G \isog L → solvable G = solvable L.
-
Lemma quotient_sol G H :
solvable G → solvable (
G / H).
+
Lemma quotient_sol G H :
solvable G → solvable (
G / H).
-
Lemma series_sol G H :
H <| G → solvable G = solvable H && solvable (
G / H).
+
Lemma series_sol G H :
H <| G → solvable G = solvable H && solvable (
G / H).
-
Lemma metacyclic_sol G :
metacyclic G → solvable G.
+
Lemma metacyclic_sol G :
metacyclic G → solvable G.
End QuotientSol.
--
cgit v1.2.3