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.extraspecial.html | 123 +++++++++++------------ 1 file changed, 61 insertions(+), 62 deletions(-) (limited to 'docs/htmldoc/mathcomp.solvable.extraspecial.html') diff --git a/docs/htmldoc/mathcomp.solvable.extraspecial.html b/docs/htmldoc/mathcomp.solvable.extraspecial.html index 4e8e995..c0f4274 100644 --- a/docs/htmldoc/mathcomp.solvable.extraspecial.html +++ b/docs/htmldoc/mathcomp.solvable.extraspecial.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.

@@ -80,58 +79,58 @@ Section Construction.

-Variable p : nat.
+Variable p : nat.

-Definition act ij (k : 'Z_p) := let: (i, j) := ij in (i + k × j, j).
-Lemma actP : is_action [set: 'Z_p] act.
+Definition act ij (k : 'Z_p) := let: (i, j) := ij in (i + k × j, j).
+Lemma actP : is_action [set: 'Z_p] act.
Canonical action := Action actP.

-Lemma gactP : is_groupAction [set: 'Z_p × 'Z_p] action.
+Lemma gactP : is_groupAction [set: 'Z_p × 'Z_p] action.
Definition groupAction := GroupAction gactP.

-Fact gtype_key : unit.
-Definition gtype := locked_with gtype_key (sdprod_groupType groupAction).
+Fact gtype_key : unit.
+Definition gtype := locked_with gtype_key (sdprod_groupType groupAction).

-Definition ngtype := ncprod [set: gtype].
+Definition ngtype := ncprod [set: gtype].

End Construction.

-Definition ngtypeQ n := xcprod [set: ngtype 2 n] 'Q_8.
+Definition ngtypeQ n := xcprod [set: ngtype 2 n] 'Q_8.

End Pextraspecial.

-Notation "p ^{1+2}" := (Pextraspecial.gtype p) : type_scope.
-Notation "p ^{1+2}" := [set: gsort p^{1+2}] : group_scope.
-Notation "p ^{1+2}" := [set: gsort p^{1+2}]%G : Group_scope.
+Notation "p ^{1+2}" := (Pextraspecial.gtype p) : type_scope.
+Notation "p ^{1+2}" := [set: gsort p^{1+2}] : group_scope.
+Notation "p ^{1+2}" := [set: gsort p^{1+2}]%G : Group_scope.

-Notation "p ^{1+2* n }" := (Pextraspecial.ngtype p n) : type_scope.
-Notation "p ^{1+2* n }" := [set: gsort p^{1+2*n}] : group_scope.
-Notation "p ^{1+2* n }" := [set: gsort p^{1+2*n}]%G : Group_scope.
+Notation "p ^{1+2* n }" := (Pextraspecial.ngtype p n) : type_scope.
+Notation "p ^{1+2* n }" := [set: gsort p^{1+2*n}] : group_scope.
+Notation "p ^{1+2* n }" := [set: gsort p^{1+2*n}]%G : Group_scope.

-Notation "''D^' n" := (Pextraspecial.ngtype 2 n) : type_scope.
-Notation "''D^' n" := [set: gsort 'D^n] : group_scope.
-Notation "''D^' n" := [set: gsort 'D^n]%G : Group_scope.
+Notation "''D^' n" := (Pextraspecial.ngtype 2 n) : type_scope.
+Notation "''D^' n" := [set: gsort 'D^n] : group_scope.
+Notation "''D^' n" := [set: gsort 'D^n]%G : Group_scope.

-Notation "''D^' n * 'Q'" := (Pextraspecial.ngtypeQ n) : type_scope.
-Notation "''D^' n * 'Q'" := [set: gsort 'D^n×Q] : group_scope.
-Notation "''D^' n * 'Q'" := [set: gsort 'D^n×Q]%G : Group_scope.
+Notation "''D^' n * 'Q'" := (Pextraspecial.ngtypeQ n) : type_scope.
+Notation "''D^' n * 'Q'" := [set: gsort 'D^n×Q] : group_scope.
+Notation "''D^' n * 'Q'" := [set: gsort 'D^n×Q]%G : Group_scope.

Section ExponentPextraspecialTheory.

-Variable p : nat.
+Variable p : nat.
Hypothesis p_pr : prime p.
Let p_gt1 := prime_gt1 p_pr.
Let p_gt0 := ltnW p_gt1.
@@ -139,14 +138,14 @@

-Lemma card_pX1p2 : #|p^{1+2}| = (p ^ 3)%N.
+Lemma card_pX1p2 : #|p^{1+2}| = (p ^ 3)%N.

Lemma Grp_pX1p2 :
-  p^{1+2} \isog Grp (x : y : (x ^+ p, y ^+ p, [~ x, y, x], [~ x, y, y])).
+  p^{1+2} \isog Grp (x : y : (x ^+ p, y ^+ p, [~ x, y, x], [~ x, y, y])).

-Lemma pX1p2_pgroup : p.-group p^{1+2}.
+Lemma pX1p2_pgroup : p.-group p^{1+2}.

@@ -155,7 +154,7 @@ This is part of the existence half of Aschbacher ex. (8.7)(1)
-Lemma pX1p2_extraspecial : extraspecial p^{1+2}.
+Lemma pX1p2_extraspecial : extraspecial p^{1+2}.

@@ -164,7 +163,7 @@ This is part of the existence half of Aschbacher ex. (8.7)(1)
-Lemma exponent_pX1p2 : odd p → exponent p^{1+2} %| p.
+Lemma exponent_pX1p2 : odd p → exponent p^{1+2} %| p.

@@ -173,8 +172,8 @@ This is the uniqueness half of Aschbacher ex. (8.7)(1)
-Lemma isog_pX1p2 (gT : finGroupType) (G : {group gT}) :
-  extraspecial G → exponent G %| p → #|G| = (p ^ 3)%N → G \isog p^{1+2}.
+Lemma isog_pX1p2 (gT : finGroupType) (G : {group gT}) :
+  extraspecial G → exponent G %| p → #|G| = (p ^ 3)%N → G \isog p^{1+2}.

End ExponentPextraspecialTheory.
@@ -183,19 +182,19 @@ Section GeneralExponentPextraspecialTheory.

-Variable p : nat.
+Variable p : nat.

-Lemma pX1p2id : p^{1+2*1} \isog p^{1+2}.
+Lemma pX1p2id : p^{1+2*1} \isog p^{1+2}.

-Lemma pX1p2S n : xcprod_spec p^{1+2} p^{1+2*n} p^{1+2*n.+1}%type.
+Lemma pX1p2S n : xcprod_spec p^{1+2} p^{1+2*n} p^{1+2*n.+1}%type.

-Lemma card_pX1p2n n : prime p → #|p^{1+2*n}| = (p ^ n.*2.+1)%N.
+Lemma card_pX1p2n n : prime p → #|p^{1+2*n}| = (p ^ n.*2.+1)%N.

-Lemma pX1p2n_pgroup n : prime p → p.-group p^{1+2*n}.
+Lemma pX1p2n_pgroup n : prime p → p.-group p^{1+2*n}.

@@ -204,7 +203,7 @@ This is part of the existence half of Aschbacher (23.13)
-Lemma exponent_pX1p2n n : prime p → odd p → exponent p^{1+2*n} = p.
+Lemma exponent_pX1p2n n : prime p → odd p → exponent p^{1+2*n} = p.

@@ -213,7 +212,7 @@ This is part of the existence half of Aschbacher (23.13) and (23.14)
-Lemma pX1p2n_extraspecial n : prime p → n > 0 → extraspecial p^{1+2*n}.
+Lemma pX1p2n_extraspecial n : prime p → n > 0 → extraspecial p^{1+2*n}.

@@ -222,16 +221,16 @@ This is Aschbacher (23.12)
-Lemma Ohm1_extraspecial_odd (gT : finGroupType) (G : {group gT}) :
-    p.-group G → extraspecial G → odd #|G| →
- let Y := 'Ohm_1(G) in
-  [/\ exponent Y = p, #|G : Y| %| p
-    & Y != G →
-      ∃ E : {group gT},
-        [/\ #|G : Y| = p, #|E| = p ∨ extraspecial E,
-            exists2 X : {group gT}, #|X| = p & X \x E = Y
-          & ∃ M : {group gT},
-             [/\ M \isog 'Mod_(p ^ 3), M \* E = G & M :&: E = 'Z(M)]]].
+Lemma Ohm1_extraspecial_odd (gT : finGroupType) (G : {group gT}) :
+    p.-group G → extraspecial G → odd #|G| →
+ let Y := 'Ohm_1(G) in
+  [/\ exponent Y = p, #|G : Y| %| p
+    & Y != G →
+      ∃ E : {group gT},
+        [/\ #|G : Y| = p, #|E| = p ∨ extraspecial E,
+            exists2 X : {group gT}, #|X| = p & X \x E = Y
+          & ∃ M : {group gT},
+             [/\ M \isog 'Mod_(p ^ 3), M \* E = G & M :&: E = 'Z(M)]]].

@@ -241,27 +240,27 @@ in part the proof that symplectic spaces are hyperbolic (19.16).
-Lemma isog_pX1p2n n (gT : finGroupType) (G : {group gT}) :
-    prime p → extraspecial G → #|G| = (p ^ n.*2.+1)%N → exponent G %| p →
-  G \isog p^{1+2*n}.
+Lemma isog_pX1p2n n (gT : finGroupType) (G : {group gT}) :
+    prime p → extraspecial G → #|G| = (p ^ n.*2.+1)%N → exponent G %| p →
+  G \isog p^{1+2*n}.

End GeneralExponentPextraspecialTheory.

-Lemma isog_2X1p2 : 2^{1+2} \isog 'D_8.
+Lemma isog_2X1p2 : 2^{1+2} \isog 'D_8.

-Lemma Q8_extraspecial : extraspecial 'Q_8.
+Lemma Q8_extraspecial : extraspecial 'Q_8.

-Lemma DnQ_P n : xcprod_spec 'D^n 'Q_8 ('D^n×Q)%type.
+Lemma DnQ_P n : xcprod_spec 'D^n 'Q_8 ('D^n×Q)%type.

-Lemma card_DnQ n : #|'D^n×Q| = (2 ^ n.+1.*2.+1)%N.
+Lemma card_DnQ n : #|'D^n×Q| = (2 ^ n.+1.*2.+1)%N.

-Lemma DnQ_pgroup n : 2.-group 'D^n×Q.
+Lemma DnQ_pgroup n : 2.-group 'D^n×Q.

@@ -270,7 +269,7 @@ Final part of the existence half of Aschbacher (23.14).
-Lemma DnQ_extraspecial n : extraspecial 'D^n×Q.
+Lemma DnQ_extraspecial n : extraspecial 'D^n×Q.

@@ -279,8 +278,8 @@ A special case of the uniqueness half of Achsbacher (23.14).
-Lemma card_isog8_extraspecial (gT : finGroupType) (G : {group gT}) :
-  #|G| = 8 → extraspecial G → (G \isog 'D_8) || (G \isog 'Q_8).
+Lemma card_isog8_extraspecial (gT : finGroupType) (G : {group gT}) :
+  #|G| = 8 → extraspecial G → (G \isog 'D_8) || (G \isog 'Q_8).

@@ -293,8 +292,8 @@ Galois theory as in (20.9) and (21.1).
-Lemma isog_2extraspecial (gT : finGroupType) (G : {group gT}) n :
-  #|G| = (2 ^ n.*2.+1)%N → extraspecial G → G \isog 'D^n ∨ G \isog 'D^n.-1×Q.
+Lemma isog_2extraspecial (gT : finGroupType) (G : {group gT}) n :
+  #|G| = (2 ^ n.*2.+1)%N → extraspecial G → G \isog 'D^n ∨ G \isog 'D^n.-1×Q.

@@ -303,7 +302,7 @@ The first concluding remark of Aschbacher (23.14).
-Lemma rank_Dn n : 'r_2('D^n) = n.+1.
+Lemma rank_Dn n : 'r_2('D^n) = n.+1.

@@ -312,7 +311,7 @@ The second concluding remark of Aschbacher (23.14).
-Lemma rank_DnQ n : 'r_2('D^n×Q) = n.+1.
+Lemma rank_DnQ n : 'r_2('D^n×Q) = n.+1.

@@ -321,7 +320,7 @@ The final concluding remark of Aschbacher (23.14).
-Lemma not_isog_Dn_DnQ n : ~~ ('D^n \isog 'D^n.-1×Q).
+Lemma not_isog_Dn_DnQ n : ~~ ('D^n \isog 'D^n.-1×Q).
-- cgit v1.2.3