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.maximal.html | 353 ++++++++++++++-------------- 1 file changed, 175 insertions(+), 178 deletions(-) (limited to 'docs/htmldoc/mathcomp.solvable.maximal.html') diff --git a/docs/htmldoc/mathcomp.solvable.maximal.html b/docs/htmldoc/mathcomp.solvable.maximal.html index af71368..ba5d392 100644 --- a/docs/htmldoc/mathcomp.solvable.maximal.html +++ b/docs/htmldoc/mathcomp.solvable.maximal.html @@ -21,7 +21,6 @@
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.

@@ -71,19 +70,19 @@
Variable gT : finGroupType.
-Implicit Types (A B D : {set gT}) (G : {group gT}).
+Implicit Types (A B D : {set gT}) (G : {group gT}).

-Definition charsimple A := [min A of G | G :!=: 1 & G \char A].
+Definition charsimple A := [min A of G | G :!=: 1 & G \char A].

-Definition Frattini A := \bigcap_(G : {group gT} | maximal_eq G A) G.
+Definition Frattini A := \bigcap_(G : {group gT} | maximal_eq G A) G.

-Canonical Frattini_group A : {group gT} := Eval hnf in [group of Frattini A].
+Canonical Frattini_group A : {group gT} := Eval hnf in [group of Frattini A].

-Definition Fitting A := \big[dprod/1]_(p <- primes #|A|) 'O_p(A).
+Definition Fitting A := \big[dprod/1]_(p <- primes #|A|) 'O_p(A).

Lemma Fitting_group_set G : group_set (Fitting G).
@@ -93,22 +92,22 @@
Definition critical A B :=
-  [/\ A \char B,
-      Frattini A \subset 'Z(A),
-      [~: B, A] \subset 'Z(A)
-   & 'C_B(A) = 'Z(A)].
+  [/\ A \char B,
+      Frattini A \subset 'Z(A),
+      [~: B, A] \subset 'Z(A)
+   & 'C_B(A) = 'Z(A)].

-Definition special A := Frattini A = 'Z(A) ∧ A^`(1) = 'Z(A).
+Definition special A := Frattini A = 'Z(A) ∧ A^`(1) = 'Z(A).

-Definition extraspecial A := special A ∧ prime #|'Z(A)|.
+Definition extraspecial A := special A ∧ prime #|'Z(A)|.

-Definition SCN B := [set A : {group gT} | A <| B & 'C_B(A) == A].
+Definition SCN B := [set A : {group gT} | A <| B & 'C_B(A) == A].

-Definition SCN_at n B := [set A in SCN B | n ≤ 'r(A)].
+Definition SCN_at n B := [set A in SCN B | n ≤ 'r(A)].

End Defs.
@@ -116,38 +115,36 @@

- -
-Notation "''Phi' ( A )" := (Frattini A)
+Notation "''Phi' ( A )" := (Frattini A)
  (at level 8, format "''Phi' ( A )") : group_scope.
-Notation "''Phi' ( G )" := (Frattini_group G) : Group_scope.
+Notation "''Phi' ( G )" := (Frattini_group G) : Group_scope.

-Notation "''F' ( G )" := (Fitting G)
+Notation "''F' ( G )" := (Fitting G)
  (at level 8, format "''F' ( G )") : group_scope.
-Notation "''F' ( G )" := (Fitting_group G) : Group_scope.
+Notation "''F' ( G )" := (Fitting_group G) : Group_scope.

-Notation "''SCN' ( B )" := (SCN B)
+Notation "''SCN' ( B )" := (SCN B)
  (at level 8, format "''SCN' ( B )") : group_scope.
-Notation "''SCN_' n ( B )" := (SCN_at n B)
+Notation "''SCN_' n ( B )" := (SCN_at n B)
  (at level 8, n at level 2, format "''SCN_' n ( B )") : group_scope.

Section PMax.

-Variables (gT : finGroupType) (p : nat) (P M : {group gT}).
-Hypothesis pP : p.-group P.
+Variables (gT : finGroupType) (p : nat) (P M : {group gT}).
+Hypothesis pP : p.-group P.

-Lemma p_maximal_normal : maximal M P → M <| P.
+Lemma p_maximal_normal : maximal M P → M <| P.

-Lemma p_maximal_index : maximal M P → #|P : M| = p.
+Lemma p_maximal_index : maximal M P → #|P : M| = p.

-Lemma p_index_maximal : M \subset P → prime #|P : M| → maximal M P.
+Lemma p_index_maximal : M \subset P → prime #|P : M| → maximal M P.

End PMax.
@@ -157,53 +154,53 @@
Variables gT : finGroupType.
-Implicit Type G M : {group gT}.
+Implicit Type G M : {group gT}.

-Lemma Phi_sub G : 'Phi(G) \subset G.
+Lemma Phi_sub G : 'Phi(G) \subset G.

-Lemma Phi_sub_max G M : maximal M G → 'Phi(G) \subset M.
+Lemma Phi_sub_max G M : maximal M G → 'Phi(G) \subset M.

-Lemma Phi_proper G : G :!=: 1 → 'Phi(G) \proper G.
+Lemma Phi_proper G : G :!=: 1 → 'Phi(G) \proper G.

-Lemma Phi_nongen G X : 'Phi(G) <*> X = G → <<X>> = G.
+Lemma Phi_nongen G X : 'Phi(G) <*> X = G → <<X>> = G.

-Lemma Frattini_continuous (rT : finGroupType) G (f : {morphism G >-> rT}) :
-  f @* 'Phi(G) \subset 'Phi(f @* G).
+Lemma Frattini_continuous (rT : finGroupType) G (f : {morphism G >-> rT}) :
+  f @* 'Phi(G) \subset 'Phi(f @* G).

End Frattini.

-Canonical Frattini_igFun := [igFun by Phi_sub & Frattini_continuous].
-Canonical Frattini_gFun := [gFun by Frattini_continuous].
+Canonical Frattini_igFun := [igFun by Phi_sub & Frattini_continuous].
+Canonical Frattini_gFun := [gFun by Frattini_continuous].

Section Frattini0.

Variable gT : finGroupType.
-Implicit Types (rT : finGroupType) (D G : {group gT}).
+Implicit Types (rT : finGroupType) (D G : {group gT}).

-Lemma Phi_char G : 'Phi(G) \char G.
+Lemma Phi_char G : 'Phi(G) \char G.

-Lemma Phi_normal G : 'Phi(G) <| G.
+Lemma Phi_normal G : 'Phi(G) <| G.

-Lemma injm_Phi rT D G (f : {morphism D >-> rT}) :
-  'injm f → G \subset D → f @* 'Phi(G) = 'Phi(f @* G).
+Lemma injm_Phi rT D G (f : {morphism D >-> rT}) :
+  'injm f → G \subset D → f @* 'Phi(G) = 'Phi(f @* G).

-Lemma isog_Phi rT G (H : {group rT}) : G \isog H → 'Phi(G) \isog 'Phi(H).
+Lemma isog_Phi rT G (H : {group rT}) : G \isog H → 'Phi(G) \isog 'Phi(H).

-Lemma PhiJ G x : 'Phi(G :^ x) = 'Phi(G) :^ x.
+Lemma PhiJ G x : 'Phi(G :^ x) = 'Phi(G) :^ x.

End Frattini0.
@@ -213,19 +210,19 @@
Variables gT : finGroupType.
-Implicit Type G : {group gT}.
+Implicit Type G : {group gT}.

-Lemma Phi_quotient_id G : 'Phi (G / 'Phi(G)) = 1.
+Lemma Phi_quotient_id G : 'Phi (G / 'Phi(G)) = 1.

-Lemma Phi_quotient_cyclic G : cyclic (G / 'Phi(G)) → cyclic G.
+Lemma Phi_quotient_cyclic G : cyclic (G / 'Phi(G)) → cyclic G.

-Variables (p : nat) (P : {group gT}).
+Variables (p : nat) (P : {group gT}).

-Lemma trivg_Phi : p.-group P → ('Phi(P) == 1) = p.-abelem P.
+Lemma trivg_Phi : p.-group P → ('Phi(P) == 1) = p.-abelem P.

End Frattini2.
@@ -234,17 +231,17 @@ Section Frattini3.

-Variables (gT : finGroupType) (p : nat) (P : {group gT}).
-Hypothesis pP : p.-group P.
+Variables (gT : finGroupType) (p : nat) (P : {group gT}).
+Hypothesis pP : p.-group P.

-Lemma Phi_quotient_abelem : p.-abelem (P / 'Phi(P)).
+Lemma Phi_quotient_abelem : p.-abelem (P / 'Phi(P)).

-Lemma Phi_joing : 'Phi(P) = P^`(1) <*> 'Mho^1(P).
+Lemma Phi_joing : 'Phi(P) = P^`(1) <*> 'Mho^1(P).

-Lemma Phi_Mho : abelian P → 'Phi(P) = 'Mho^1(P).
+Lemma Phi_Mho : abelian P → 'Phi(P) = 'Mho^1(P).

End Frattini3.
@@ -253,19 +250,19 @@ Section Frattini4.

-Variables (p : nat) (gT : finGroupType).
-Implicit Types (rT : finGroupType) (P G H K D : {group gT}).
+Variables (p : nat) (gT : finGroupType).
+Implicit Types (rT : finGroupType) (P G H K D : {group gT}).

-Lemma PhiS G H : p.-group H → G \subset H → 'Phi(G) \subset 'Phi(H).
+Lemma PhiS G H : p.-group H → G \subset H → 'Phi(G) \subset 'Phi(H).

-Lemma morphim_Phi rT P D (f : {morphism D >-> rT}) :
-  p.-group P → P \subset D → f @* 'Phi(P) = 'Phi(f @* P).
+Lemma morphim_Phi rT P D (f : {morphism D >-> rT}) :
+  p.-group P → P \subset D → f @* 'Phi(P) = 'Phi(f @* P).

Lemma quotient_Phi P H :
-  p.-group P → P \subset 'N(H) → 'Phi(P) / H = 'Phi(P / H).
+  p.-group P → P \subset 'N(H) → 'Phi(P) / H = 'Phi(P / H).

@@ -275,20 +272,20 @@
Lemma Phi_min G H :
-  p.-group G → G \subset 'N(H) → p.-abelem (G / H) → 'Phi(G) \subset H.
+  p.-group G → G \subset 'N(H) → p.-abelem (G / H) → 'Phi(G) \subset H.

Lemma Phi_cprod G H K :
-  p.-group G → H \* K = G → 'Phi(H) \* 'Phi(K) = 'Phi(G).
+  p.-group G → H \* K = G → 'Phi(H) \* 'Phi(K) = 'Phi(G).

Lemma Phi_mulg H K :
-    p.-group H → p.-group K → K \subset 'C(H) →
-  'Phi(H × K) = 'Phi(H) × 'Phi(K).
+    p.-group H → p.-group K → K \subset 'C(H) →
+  'Phi(H × K) = 'Phi(H) × 'Phi(K).

Lemma charsimpleP G :
-  reflect (G :!=: 1 ∧ ∀ K, K :!=: 1 → K \char G → K :=: G)
+  reflect (G :!=: 1 ∧ ∀ K, K :!=: 1 → K \char G → K :=: G)
          (charsimple G).

@@ -299,35 +296,35 @@
Variable gT : finGroupType.
-Implicit Types (p : nat) (G H : {group gT}).
+Implicit Types (p : nat) (G H : {group gT}).

-Lemma Fitting_normal G : 'F(G) <| G.
+Lemma Fitting_normal G : 'F(G) <| G.

-Lemma Fitting_sub G : 'F(G) \subset G.
+Lemma Fitting_sub G : 'F(G) \subset G.

-Lemma Fitting_nil G : nilpotent 'F(G).
+Lemma Fitting_nil G : nilpotent 'F(G).

-Lemma Fitting_max G H : H <| G → nilpotent H → H \subset 'F(G).
+Lemma Fitting_max G H : H <| G → nilpotent H → H \subset 'F(G).

-Lemma pcore_Fitting pi G : 'O_pi('F(G)) \subset 'O_pi(G).
+Lemma pcore_Fitting pi G : 'O_pi('F(G)) \subset 'O_pi(G).

-Lemma p_core_Fitting p G : 'O_p('F(G)) = 'O_p(G).
+Lemma p_core_Fitting p G : 'O_p('F(G)) = 'O_p(G).

-Lemma nilpotent_Fitting G : nilpotent G → 'F(G) = G.
+Lemma nilpotent_Fitting G : nilpotent G → 'F(G) = G.

-Lemma Fitting_eq_pcore p G : 'O_p^'(G) = 1 → 'F(G) = 'O_p(G).
+Lemma Fitting_eq_pcore p G : 'O_p^'(G) = 1 → 'F(G) = 'O_p(G).

Lemma FittingEgen G :
-  'F(G) = <<\bigcup_(p < #|G|.+1 | (p : nat) \in \pi(G)) 'O_p(G)>>.
+  'F(G) = <<\bigcup_(p < #|G|.+1 | (p : nat) \in \pi(G)) 'O_p(G)>>.

End Fitting.
@@ -339,36 +336,36 @@ Implicit Types gT rT : finGroupType.

-Lemma morphim_Fitting : GFunctor.pcontinuous Fitting.
+Lemma morphim_Fitting : GFunctor.pcontinuous (@Fitting).

-Lemma FittingS gT (G H : {group gT}) : H \subset G → H :&: 'F(G) \subset 'F(H).
+Lemma FittingS gT (G H : {group gT}) : H \subset G → H :&: 'F(G) \subset 'F(H).

-Lemma FittingJ gT (G : {group gT}) x : 'F(G :^ x) = 'F(G) :^ x.
+Lemma FittingJ gT (G : {group gT}) x : 'F(G :^ x) = 'F(G) :^ x.

End FittingFun.

-Canonical Fitting_igFun := [igFun by Fitting_sub & morphim_Fitting].
-Canonical Fitting_gFun := [gFun by morphim_Fitting].
-Canonical Fitting_pgFun := [pgFun by morphim_Fitting].
+Canonical Fitting_igFun := [igFun by Fitting_sub & morphim_Fitting].
+Canonical Fitting_gFun := [gFun by morphim_Fitting].
+Canonical Fitting_pgFun := [pgFun by morphim_Fitting].

Section IsoFitting.

-Variables (gT rT : finGroupType) (G D : {group gT}) (f : {morphism D >-> rT}).
+Variables (gT rT : finGroupType) (G D : {group gT}) (f : {morphism D >-> rT}).

-Lemma Fitting_char : 'F(G) \char G.
+Lemma Fitting_char : 'F(G) \char G.

-Lemma injm_Fitting : 'injm f → G \subset D → f @* 'F(G) = 'F(f @* G).
+Lemma injm_Fitting : 'injm f → G \subset D → f @* 'F(G) = 'F(f @* G).

-Lemma isog_Fitting (H : {group rT}) : G \isog H → 'F(G) \isog 'F(H).
+Lemma isog_Fitting (H : {group rT}) : G \isog H → 'F(G) \isog 'F(H).

End IsoFitting.
@@ -378,54 +375,54 @@
Variable gT : finGroupType.
-Implicit Types (rT : finGroupType) (G H K L : {group gT}) (p : nat).
+Implicit Types (rT : finGroupType) (G H K L : {group gT}) (p : nat).

-Lemma minnormal_charsimple G H : minnormal H G → charsimple H.
+Lemma minnormal_charsimple G H : minnormal H G → charsimple H.

Lemma maxnormal_charsimple G H L :
-  G <| L → maxnormal H G L → charsimple (G / H).
+  G <| L → maxnormal H G L → charsimple (G / H).

-Lemma abelem_split_dprod rT p (A B : {group rT}) :
-  p.-abelem A → B \subset A → ∃ C : {group rT}, B \x C = A.
+Lemma abelem_split_dprod rT p (A B : {group rT}) :
+  p.-abelem A → B \subset A → ∃ C : {group rT}, B \x C = A.

-Lemma p_abelem_split1 rT p (A : {group rT}) x :
-     p.-abelem A → x \in A →
-  ∃ B : {group rT}, [/\ B \subset A, #|B| = #|A| %/ #[x] & <[x]> \x B = A].
+Lemma p_abelem_split1 rT p (A : {group rT}) x :
+     p.-abelem A → x \in A →
+  ∃ B : {group rT}, [/\ B \subset A, #|B| = #|A| %/ #[x] & <[x]> \x B = A].

-Lemma abelem_charsimple p G : p.-abelem G → G :!=: 1 → charsimple G.
+Lemma abelem_charsimple p G : p.-abelem G → G :!=: 1 → charsimple G.

-Lemma charsimple_dprod G : charsimple G →
-  ∃ H : {group gT}, [/\ H \subset G, simple H
-                         & exists2 I : {set {perm gT}}, I \subset Aut G
-                         & \big[dprod/1]_(f in I) f @: H = G].
+Lemma charsimple_dprod G : charsimple G →
+  ∃ H : {group gT}, [/\ H \subset G, simple H
+                         & exists2 I : {set {perm gT}}, I \subset Aut G
+                         & \big[dprod/1]_(f in I) f @: H = G].

-Lemma simple_sol_prime G : solvable G → simple G → prime #|G|.
+Lemma simple_sol_prime G : solvable G → simple G → prime #|G|.

-Lemma charsimple_solvable G : charsimple G → solvable G → is_abelem G.
+Lemma charsimple_solvable G : charsimple G → solvable G → is_abelem G.

Lemma minnormal_solvable L G H :
-    minnormal H L → H \subset G → solvable G →
-  [/\ L \subset 'N(H), H :!=: 1 & is_abelem H].
+    minnormal H L → H \subset G → solvable G →
+  [/\ L \subset 'N(H), H :!=: 1 & is_abelem H].

Lemma solvable_norm_abelem L G :
-    solvable G → G <| L → G :!=: 1 →
-  ∃ H : {group gT}, [/\ H \subset G, H <| L, H :!=: 1 & is_abelem H].
+    solvable G → G <| L → G :!=: 1 →
+  ∃ H : {group gT}, [/\ H \subset G, H <| L, H :!=: 1 & is_abelem H].

-Lemma trivg_Fitting G : solvable G → ('F(G) == 1) = (G :==: 1).
+Lemma trivg_Fitting G : solvable G → ('F(G) == 1) = (G :==: 1).

-Lemma Fitting_pcore pi G : 'F('O_pi(G)) = 'O_pi('F(G)).
+Lemma Fitting_pcore pi G : 'F('O_pi(G)) = 'O_pi('F(G)).

End CharSimple.
@@ -434,15 +431,15 @@ Section SolvablePrimeFactor.

-Variables (gT : finGroupType) (G : {group gT}).
+Variables (gT : finGroupType) (G : {group gT}).

-Lemma index_maxnormal_sol_prime (H : {group gT}) :
-  solvable G → maxnormal H G G → prime #|G : H|.
+Lemma index_maxnormal_sol_prime (H : {group gT}) :
+  solvable G → maxnormal H G G → prime #|G : H|.

Lemma sol_prime_factor_exists :
-  solvable G → G :!=: 1 → {H : {group gT} | H <| G & prime #|G : H| }.
+  solvable G → G :!=: 1 → {H : {group gT} | H <| G & prime #|G : H| }.

End SolvablePrimeFactor.
@@ -451,7 +448,7 @@ Section Special.

-Variables (gT : finGroupType) (p : nat) (A G : {group gT}).
+Variables (gT : finGroupType) (p : nat) (A G : {group gT}).

@@ -460,10 +457,10 @@ This is Aschbacher (23.7)
-Lemma center_special_abelem : p.-group G → special G → p.-abelem 'Z(G).
+Lemma center_special_abelem : p.-group G → special G → p.-abelem 'Z(G).

-Lemma exponent_special : p.-group G → special G → exponent G %| p ^ 2.
+Lemma exponent_special : p.-group G → special G → exponent G %| p ^ 2.

@@ -473,9 +470,9 @@
Theorem abelian_charsimple_special :
-    p.-group G → coprime #|G| #|A| → [~: G, A] = G →
-    \bigcup_(H : {group gT} | (H \char G) && abelian H) H \subset 'C(A) →
-  special G ∧ 'C_G(A) = 'Z(G).
+    p.-group G → coprime #|G| #|A| → [~: G, A] = G →
+    \bigcup_(H : {group gT} | (H \char G) && abelian H) H \subset 'C(A) →
+  special G ∧ 'C_G(A) = 'Z(G).

End Special.
@@ -484,63 +481,63 @@ Section Extraspecial.

-Variables (p : nat) (gT rT : finGroupType).
-Implicit Types D E F G H K M R S T U : {group gT}.
+Variables (p : nat) (gT rT : finGroupType).
+Implicit Types D E F G H K M R S T U : {group gT}.

Section Basic.

-Variable S : {group gT}.
-Hypotheses (pS : p.-group S) (esS : extraspecial S).
+Variable S : {group gT}.
+Hypotheses (pS : p.-group S) (esS : extraspecial S).

-Let pZ : p.-group 'Z(S) := pgroupS (center_sub S) pS.
+Let pZ : p.-group 'Z(S) := pgroupS (center_sub S) pS.
Lemma extraspecial_prime : prime p.

-Lemma card_center_extraspecial : #|'Z(S)| = p.
+Lemma card_center_extraspecial : #|'Z(S)| = p.

-Lemma min_card_extraspecial : #|S| ≥ p ^ 3.
+Lemma min_card_extraspecial : #|S| ≥ p ^ 3.

End Basic.

Lemma card_p3group_extraspecial E :
-  prime p → #|E| = (p ^ 3)%N → #|'Z(E)| = p → extraspecial E.
+  prime p → #|E| = (p ^ 3)%N → #|'Z(E)| = p → extraspecial E.

Lemma p3group_extraspecial G :
-  p.-group G → ~~ abelian G → logn p #|G| ≤ 3 → extraspecial G.
+  p.-group G → ~~ abelian G → logn p #|G| ≤ 3 → extraspecial G.

-Lemma extraspecial_nonabelian G : extraspecial G → ~~ abelian G.
+Lemma extraspecial_nonabelian G : extraspecial G → ~~ abelian G.

-Lemma exponent_2extraspecial G : 2.-group G → extraspecial G → exponent G = 4.
+Lemma exponent_2extraspecial G : 2.-group G → extraspecial G → exponent G = 4.

-Lemma injm_special D G (f : {morphism D >-> rT}) :
-  'injm f → G \subset D → special G → special (f @* G).
+Lemma injm_special D G (f : {morphism D >-> rT}) :
+  'injm f → G \subset D → special G → special (f @* G).

-Lemma injm_extraspecial D G (f : {morphism D >-> rT}) :
-  'injm f → G \subset D → extraspecial G → extraspecial (f @* G).
+Lemma injm_extraspecial D G (f : {morphism D >-> rT}) :
+  'injm f → G \subset D → extraspecial G → extraspecial (f @* G).

-Lemma isog_special G (R : {group rT}) :
-  G \isog R → special G → special R.
+Lemma isog_special G (R : {group rT}) :
+  G \isog R → special G → special R.

-Lemma isog_extraspecial G (R : {group rT}) :
-  G \isog R → extraspecial G → extraspecial R.
+Lemma isog_extraspecial G (R : {group rT}) :
+  G \isog R → extraspecial G → extraspecial R.

Lemma cprod_extraspecial G H K :
-    p.-group G → H \* K = G → H :&: K = 'Z(H) →
-  extraspecial H → extraspecial K → extraspecial G.
+    p.-group G → H \* K = G → H :&: K = 'Z(H) →
+  extraspecial H → extraspecial K → extraspecial G.

@@ -552,8 +549,8 @@ Section ExtraspecialFormspace.

-Variable G : {group gT}.
-Hypotheses (pG : p.-group G) (esG : extraspecial G).
+Variable G : {group gT}.
+Hypotheses (pG : p.-group G) (esG : extraspecial G).

Let p_pr := extraspecial_prime pG esG.
@@ -569,7 +566,7 @@
Lemma cent1_extraspecial_maximal x :
-  x \in G → x \notin 'Z(G) → maximal 'C_G[x] G.
+  x \in G → x \notin 'Z(G) → maximal 'C_G[x] G.

@@ -580,7 +577,7 @@
Lemma subcent1_extraspecial_maximal U x :
-  U \subset G → x \in G :\: 'C(U) → maximal 'C_U[x] U.
+  U \subset G → x \in G :\: 'C(U) → maximal 'C_U[x] U.

@@ -591,7 +588,7 @@
Lemma card_subcent_extraspecial U :
-  U \subset G → #|'C_G(U)| = (#|'Z(G) :&: U| × #|G : U|)%N.
+  U \subset G → #|'C_G(U)| = (#|'Z(G) :&: U| × #|G : U|)%N.

@@ -603,13 +600,13 @@
Lemma split1_extraspecial x :
-    x \in G :\: 'Z(G) →
-  {E : {group gT} & {R : {group gT} |
-    [/\ #|E| = (p ^ 3)%N ∧ #|R| = #|G| %/ p ^ 2,
-        E \* R = G ∧ E :&: R = 'Z(E),
-        'Z(E) = 'Z(G) ∧ 'Z(R) = 'Z(G),
-        extraspecial E ∧ x \in E
-      & if abelian R then R :=: 'Z(G) else extraspecial R]}}.
+    x \in G :\: 'Z(G) →
+  {E : {group gT} & {R : {group gT} |
+    [/\ #|E| = (p ^ 3)%N ∧ #|R| = #|G| %/ p ^ 2,
+        E \* R = G ∧ E :&: R = 'Z(E),
+        'Z(E) = 'Z(G) ∧ 'Z(R) = 'Z(G),
+        extraspecial E ∧ x \in E
+      & if abelian R then R :=: 'Z(G) else extraspecial R]}}.

@@ -622,7 +619,7 @@ Note that Aschbacher derives this from the Witt lemma, which we avoid.
-Lemma pmaxElem_extraspecial : 'E×_p(G) = 'E_p^('r_p(G))(G).
+Lemma pmaxElem_extraspecial : 'E×_p(G) = 'E_p^('r_p(G))(G).

End ExtraspecialFormspace.
@@ -635,8 +632,8 @@
Lemma critical_extraspecial R S :
-    p.-group R → S \subset R → extraspecial S → [~: S, R] \subset S^`(1) →
-  S \* 'C_R(S) = R.
+    p.-group R → S \subset R → extraspecial S → [~: S, R] \subset S^`(1) →
+  S \* 'C_R(S) = R.

@@ -645,16 +642,16 @@ This is part of Aschbacher (23.13) and (23.14).
-Theorem extraspecial_structure S : p.-group S → extraspecial S →
-  {Es | all (fun E ⇒ (#|E| == p ^ 3)%N && ('Z(E) == 'Z(S))) Es
-      & \big[cprod/1%g]_(E <- Es) E \* 'Z(S) = S}.
+Theorem extraspecial_structure S : p.-group S → extraspecial S →
+  {Es | all (fun E ⇒ (#|E| == p ^ 3)%N && ('Z(E) == 'Z(S))) Es
+      & \big[cprod/1%g]_(E <- Es) E \* 'Z(S) = S}.

Section StructureCorollaries.

-Variable S : {group gT}.
-Hypotheses (pS : p.-group S) (esS : extraspecial S).
+Variable S : {group gT}.
+Hypotheses (pS : p.-group S) (esS : extraspecial S).

Let p_pr := extraspecial_prime pS esS.
@@ -667,10 +664,10 @@ This is Aschbacher (23.10)(2).
-Lemma card_extraspecial : {n | n > 0 & #|S| = (p ^ n.*2.+1)%N}.
+Lemma card_extraspecial : {n | n > 0 & #|S| = (p ^ n.*2.+1)%N}.

-Lemma Aut_extraspecial_full : Aut_in (Aut S) 'Z(S) \isog Aut 'Z(S).
+Lemma Aut_extraspecial_full : Aut_in (Aut S) 'Z(S) \isog Aut 'Z(S).

@@ -681,8 +678,8 @@ quoted from Gorenstein in the proof of B & G, Theorem 2.5.
-Lemma center_aut_extraspecial k : coprime k p →
-  exists2 f, f \in Aut S & ∀ z, z \in 'Z(S) → f z = (z ^+ k)%g.
+Lemma center_aut_extraspecial k : coprime k p →
+  exists2 f, f \in Aut S & ∀ z, z \in 'Z(S) → f z = (z ^+ k)%g.

End StructureCorollaries.
@@ -694,18 +691,18 @@ Section SCN.

-Variables (gT : finGroupType) (p : nat) (G : {group gT}).
-Implicit Types A Z H : {group gT}.
+Variables (gT : finGroupType) (p : nat) (G : {group gT}).
+Implicit Types A Z H : {group gT}.

-Lemma SCN_P A : reflect (A <| G ∧ 'C_G(A) = A) (A \in 'SCN(G)).
+Lemma SCN_P A : reflect (A <| G ∧ 'C_G(A) = A) (A \in 'SCN(G)).

-Lemma SCN_abelian A : A \in 'SCN(G) → abelian A.
+Lemma SCN_abelian A : A \in 'SCN(G) → abelian A.

Lemma exponent_Ohm1_class2 H :
-  odd p → p.-group H → nil_class H ≤ 2 → exponent 'Ohm_1(H) %| p.
+  odd p → p.-group H → nil_class H ≤ 2 → exponent 'Ohm_1(H) %| p.

@@ -714,11 +711,11 @@ SCN_max and max_SCN cover Aschbacher 23.15(1)
-Lemma SCN_max A : A \in 'SCN(G) → [max A | A <| G & abelian A].
+Lemma SCN_max A : A \in 'SCN(G) → [max A | A <| G & abelian A].

Lemma max_SCN A :
-  p.-group G → [max A | A <| G & abelian A] → A \in 'SCN(G).
+  p.-group G → [max A | A <| G & abelian A] → A \in 'SCN(G).

@@ -733,14 +730,14 @@ Section SCNseries.

-Variables A : {group gT}.
-Hypothesis SCN_A : A \in 'SCN(G).
+Variables A : {group gT}.
+Hypothesis SCN_A : A \in 'SCN(G).

-Let Z := 'Ohm_1(A).
+Let Z := 'Ohm_1(A).
Let cAA := SCN_abelian SCN_A.
-Let sZA: Z \subset A := Ohm_sub 1 A.
-Let nZA : A \subset 'N(Z) := sub_abelian_norm cAA sZA.
+Let sZA: Z \subset A := Ohm_sub 1 A.
+Let nZA : A \subset 'N(Z) := sub_abelian_norm cAA sZA.

@@ -749,7 +746,7 @@ This is Aschbacher 23.15(2).
-Lemma der1_stab_Ohm1_SCN_series : ('C(Z) :&: 'C_G(A / Z | 'Q))^`(1) \subset A.
+Lemma der1_stab_Ohm1_SCN_series : ('C(Z) :&: 'C_G(A / Z | 'Q))^`(1) \subset A.

@@ -760,7 +757,7 @@
Lemma Ohm1_stab_Ohm1_SCN_series :
-  odd p → p.-group G → 'Ohm_1('C_G(Z)) \subset 'C_G(A / Z | 'Q).
+  odd p → p.-group G → 'Ohm_1('C_G(Z)) \subset 'C_G(A / Z | 'Q).

End SCNseries.
@@ -773,10 +770,10 @@
Lemma Ohm1_cent_max_normal_abelem Z :
-  odd p → p.-group G → [max Z | Z <| G & p.-abelem Z] → 'Ohm_1('C_G(Z)) = Z.
+  odd p → p.-group G → [max Z | Z <| G & p.-abelem Z] → 'Ohm_1('C_G(Z)) = Z.

-Lemma critical_class2 H : critical H G → nil_class H ≤ 2.
+Lemma critical_class2 H : critical H G → nil_class H ≤ 2.

@@ -785,11 +782,11 @@ This proof of the Thompson critical lemma is adapted from Aschbacher 23.6
-Lemma Thompson_critical : p.-group G → {K : {group gT} | critical K G}.
+Lemma Thompson_critical : p.-group G → {K : {group gT} | critical K G}.

Lemma critical_p_stab_Aut H :
-  critical H G → p.-group G → p.-group 'C(H | [Aut G]).
+  critical H G → p.-group G → p.-group 'C(H | [Aut G]).

End SCN.
-- cgit v1.2.3