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.hall.html | 179 +++++++++++++++---------------- 1 file changed, 89 insertions(+), 90 deletions(-) (limited to 'docs/htmldoc/mathcomp.solvable.hall.html') diff --git a/docs/htmldoc/mathcomp.solvable.hall.html b/docs/htmldoc/mathcomp.solvable.hall.html index f75c680..b7a1b3b 100644 --- a/docs/htmldoc/mathcomp.solvable.hall.html +++ b/docs/htmldoc/mathcomp.solvable.hall.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.

@@ -52,26 +51,26 @@ Implicit Type gT : finGroupType.

-Theorem SchurZassenhaus_split gT (G H : {group gT}) :
-  Hall G H → H <| G → [splits G, over H].
+Theorem SchurZassenhaus_split gT (G H : {group gT}) :
+  Hall G H → H <| G → [splits G, over H].

-Theorem SchurZassenhaus_trans_sol gT (H K K1 : {group gT}) :
-    solvable H → K \subset 'N(H) → K1 \subset H × K →
-    coprime #|H| #|K| → #|K1| = #|K| →
-  exists2 x, x \in H & K1 :=: K :^ x.
+Theorem SchurZassenhaus_trans_sol gT (H K K1 : {group gT}) :
+    solvable H → K \subset 'N(H) → K1 \subset H × K →
+    coprime #|H| #|K| → #|K1| = #|K| →
+  exists2 x, x \in H & K1 :=: K :^ x.

-Lemma SchurZassenhaus_trans_actsol gT (G A B : {group gT}) :
-    solvable A → A \subset 'N(G) → B \subset A <*> G →
-    coprime #|G| #|A| → #|A| = #|B| →
-  exists2 x, x \in G & B :=: A :^ x.
+Lemma SchurZassenhaus_trans_actsol gT (G A B : {group gT}) :
+    solvable A → A \subset 'N(G) → B \subset A <*> G →
+    coprime #|G| #|A| → #|A| = #|B| →
+  exists2 x, x \in G & B :=: A :^ x.

-Lemma Hall_exists_subJ pi gT (G : {group gT}) :
-  solvable G → exists2 H : {group gT}, pi.-Hall(G) H
-                & ∀ K : {group gT}, K \subset G → pi.-group K →
-                  exists2 x, x \in G & K \subset H :^ x.
+Lemma Hall_exists_subJ pi gT (G : {group gT}) :
+  solvable G → exists2 H : {group gT}, pi.-Hall(G) H
+                & ∀ K : {group gT}, K \subset G → pi.-group K →
+                  exists2 x, x \in G & K \subset H :^ x.

End Hall.
@@ -83,32 +82,32 @@ Variable gT : finGroupType.

-Corollary Hall_exists pi (G : {group gT}) :
-  solvable G → ∃ H : {group gT}, pi.-Hall(G) H.
+Corollary Hall_exists pi (G : {group gT}) :
+  solvable G → ∃ H : {group gT}, pi.-Hall(G) H.

-Corollary Hall_trans pi (G H1 H2 : {group gT}) :
-  solvable G → pi.-Hall(G) H1 → pi.-Hall(G) H2 →
-  exists2 x, x \in G & H1 :=: H2 :^ x.
+Corollary Hall_trans pi (G H1 H2 : {group gT}) :
+  solvable G → pi.-Hall(G) H1 → pi.-Hall(G) H2 →
+  exists2 x, x \in G & H1 :=: H2 :^ x.

-Corollary Hall_superset pi (G K : {group gT}) :
-  solvable G → K \subset G → pi.-group K →
-    exists2 H : {group gT}, pi.-Hall(G) H & K \subset H.
+Corollary Hall_superset pi (G K : {group gT}) :
+  solvable G → K \subset G → pi.-group K →
+    exists2 H : {group gT}, pi.-Hall(G) H & K \subset H.

-Corollary Hall_subJ pi (G H K : {group gT}) :
-    solvable G → pi.-Hall(G) H → K \subset G → pi.-group K →
-  exists2 x, x \in G & K \subset H :^ x.
+Corollary Hall_subJ pi (G H K : {group gT}) :
+    solvable G → pi.-Hall(G) H → K \subset G → pi.-group K →
+  exists2 x, x \in G & K \subset H :^ x.

-Corollary Hall_Jsub pi (G H K : {group gT}) :
-    solvable G → pi.-Hall(G) H → K \subset G → pi.-group K →
-  exists2 x, x \in G & K :^ x \subset H.
+Corollary Hall_Jsub pi (G H K : {group gT}) :
+    solvable G → pi.-Hall(G) H → K \subset G → pi.-group K →
+  exists2 x, x \in G & K :^ x \subset H.

-Lemma Hall_Frattini_arg pi (G K H : {group gT}) :
-  solvable K → K <| G → pi.-Hall(K) H → K × 'N_G(H) = G.
+Lemma Hall_Frattini_arg pi (G K H : {group gT}) :
+  solvable K → K <| G → pi.-Hall(K) H → K × 'N_G(H) = G.

End HallCorollaries.
@@ -118,7 +117,7 @@
Variables (pi : nat_pred) (gT : finGroupType).
-Implicit Types G H K A X : {group gT}.
+Implicit Types G H K A X : {group gT}.

@@ -128,7 +127,7 @@
Lemma coprime_norm_cent A G :
-  A \subset 'N(G) → coprime #|G| #|A| → 'N_G(A) = 'C_G(A).
+  A \subset 'N(G) → coprime #|G| #|A| → 'N_G(A) = 'C_G(A).

@@ -138,8 +137,8 @@
Proposition coprime_Hall_exists A G :
-    A \subset 'N(G) → coprime #|G| #|A| → solvable G →
-  exists2 H : {group gT}, pi.-Hall(G) H & A \subset 'N(H).
+    A \subset 'N(G) → coprime #|G| #|A| → solvable G →
+  exists2 H : {group gT}, pi.-Hall(G) H & A \subset 'N(H).

@@ -149,10 +148,10 @@
Proposition coprime_Hall_trans A G H1 H2 :
-    A \subset 'N(G) → coprime #|G| #|A| → solvable G →
-    pi.-Hall(G) H1 → A \subset 'N(H1) →
-    pi.-Hall(G) H2 → A \subset 'N(H2) →
-  exists2 x, x \in 'C_G(A) & H1 :=: H2 :^ x.
+    A \subset 'N(G) → coprime #|G| #|A| → solvable G →
+    pi.-Hall(G) H1 → A \subset 'N(H1) →
+    pi.-Hall(G) H2 → A \subset 'N(H2) →
+  exists2 x, x \in 'C_G(A) & H1 :=: H2 :^ x.

@@ -161,8 +160,8 @@ A complement to the above: 'C(A) acts on 'Nby(A)
-Lemma norm_conj_cent A G x : x \in 'C(A) →
-  (A \subset 'N(G :^ x)) = (A \subset 'N(G)).
+Lemma norm_conj_cent A G x : x \in 'C(A) →
+  (A \subset 'N(G :^ x)) = (A \subset 'N(G)).

@@ -174,10 +173,10 @@
Lemma strongest_coprime_quotient_cent A G H :
-      let R := H :&: [~: G, A] in
-      A \subset 'N(H) → R \subset G → coprime #|R| #|A| →
-      solvable R || solvable A →
-  'C_G(A) / H = 'C_(G / H)(A / H).
+      let R := H :&: [~: G, A] in
+      A \subset 'N(H) → R \subset G → coprime #|R| #|A| →
+      solvable R || solvable A →
+  'C_G(A) / H = 'C_(G / H)(A / H).

@@ -192,8 +191,8 @@
Lemma coprime_norm_quotient_cent A G H :
-    A \subset 'N(G) → A \subset 'N(H) → coprime #|H| #|A| → solvable H →
-  'C_G(A) / H = 'C_(G / H)(A / H).
+    A \subset 'N(G) → A \subset 'N(H) → coprime #|H| #|A| → solvable H →
+  'C_G(A) / H = 'C_(G / H)(A / H).

@@ -204,9 +203,9 @@
Lemma coprime_cent_mulG A G H :
-     A \subset 'N(G) → A \subset 'N(H) → G \subset 'N(H) →
-     coprime #|H| #|A| → solvable H →
-  'C_(H × G)(A) = 'C_H(A) × 'C_G(A).
+     A \subset 'N(G) → A \subset 'N(H) → G \subset 'N(H) →
+     coprime #|H| #|A| → solvable H →
+  'C_(H × G)(A) = 'C_H(A) × 'C_G(A).

@@ -218,8 +217,8 @@
Lemma quotient_TI_subcent K G H :
-    G \subset 'N(K) → G \subset 'N(H) → K :&: H = 1 →
-  'C_K(G) / H = 'C_(K / H)(G / H).
+    G \subset 'N(K) → G \subset 'N(H) → K :&: H = 1 →
+  'C_K(G) / H = 'C_(K / H)(G / H).

@@ -231,8 +230,8 @@
Proposition coprime_quotient_cent A G H :
-    H \subset G → A \subset 'N(H) → coprime #|G| #|A| → solvable G →
-  'C_G(A) / H = 'C_(G / H)(A / H).
+    H \subset G → A \subset 'N(H) → coprime #|G| #|A| → solvable G →
+  'C_G(A) / H = 'C_(G / H)(A / H).

@@ -242,9 +241,9 @@
Proposition coprime_comm_pcore A G K :
-    A \subset 'N(G) → coprime #|G| #|A| → solvable G →
-    pi^'.-Hall(G) K → K \subset 'C_G(A) →
-  [~: G, A] \subset 'O_pi(G).
+    A \subset 'N(G) → coprime #|G| #|A| → solvable G →
+    pi^'.-Hall(G) K → K \subset 'C_G(A) →
+  [~: G, A] \subset 'O_pi(G).

End InternalAction.
@@ -256,30 +255,30 @@ This is B & G, Proposition 1.5(b).
-Proposition coprime_Hall_subset pi (gT : finGroupType) (A G X : {group gT}) :
-    A \subset 'N(G) → coprime #|G| #|A| → solvable G →
-    X \subset G → pi.-group X → A \subset 'N(X) →
-  ∃ H : {group gT}, [/\ pi.-Hall(G) H, A \subset 'N(H) & X \subset H].
+Proposition coprime_Hall_subset pi (gT : finGroupType) (A G X : {group gT}) :
+    A \subset 'N(G) → coprime #|G| #|A| → solvable G →
+    X \subset G → pi.-group X → A \subset 'N(X) →
+  ∃ H : {group gT}, [/\ pi.-Hall(G) H, A \subset 'N(H) & X \subset H].

Section ExternalAction.

Variables (pi : nat_pred) (aT gT : finGroupType).
-Variables (A : {group aT}) (G : {group gT}) (to : groupAction A G).
+Variables (A : {group aT}) (G : {group gT}) (to : groupAction A G).

Section FullExtension.

-Let injG : 'injm inG := injm_sdpair1 _.
-Let injA : 'injm inA := injm_sdpair2 _.
+Let injG : 'injm inG := injm_sdpair1 _.
+Let injA : 'injm inA := injm_sdpair2 _.

-Hypotheses (coGA : coprime #|G| #|A|) (solG : solvable G).
+Hypotheses (coGA : coprime #|G| #|A|) (solG : solvable G).

-Lemma external_action_im_coprime : coprime #|G'| #|A'|.
+Lemma external_action_im_coprime : coprime #|G'| #|A'|.

Let coGA' := external_action_im_coprime.
@@ -292,24 +291,24 @@
Lemma ext_coprime_Hall_exists :
-  exists2 H : {group gT}, pi.-Hall(G) H & [acts A, on H | to].
+  exists2 H : {group gT}, pi.-Hall(G) H & [acts A, on H | to].

-Lemma ext_coprime_Hall_trans (H1 H2 : {group gT}) :
-    pi.-Hall(G) H1 → [acts A, on H1 | to] →
-    pi.-Hall(G) H2 → [acts A, on H2 | to] →
-  exists2 x, x \in 'C_(G | to)(A) & H1 :=: H2 :^ x.
+Lemma ext_coprime_Hall_trans (H1 H2 : {group gT}) :
+    pi.-Hall(G) H1 → [acts A, on H1 | to] →
+    pi.-Hall(G) H2 → [acts A, on H2 | to] →
+  exists2 x, x \in 'C_(G | to)(A) & H1 :=: H2 :^ x.

-Lemma ext_norm_conj_cent (H : {group gT}) x :
-    H \subset G → x \in 'C_(G | to)(A) →
-  [acts A, on H :^ x | to] = [acts A, on H | to].
+Lemma ext_norm_conj_cent (H : {group gT}) x :
+    H \subset G → x \in 'C_(G | to)(A) →
+  [acts A, on H :^ x | to] = [acts A, on H | to].

-Lemma ext_coprime_Hall_subset (X : {group gT}) :
-    X \subset G → pi.-group X → [acts A, on X | to] →
-  ∃ H : {group gT},
-    [/\ pi.-Hall(G) H, [acts A, on H | to] & X \subset H].
+Lemma ext_coprime_Hall_subset (X : {group gT}) :
+    X \subset G → pi.-group X → [acts A, on X | to] →
+  ∃ H : {group gT},
+    [/\ pi.-Hall(G) H, [acts A, on H | to] & X \subset H].

End FullExtension.
@@ -325,9 +324,9 @@ we do not require that G normalize H.
-Lemma ext_coprime_quotient_cent (H : {group gT}) :
-    H \subset G → [acts A, on H | to] → coprime #|H| #|A| → solvable H →
- 'C_(|to)(A) / H = 'C_(|to / H)(A).
+Lemma ext_coprime_quotient_cent (H : {group gT}) :
+    H \subset G → [acts A, on H | to] → coprime #|H| #|A| → solvable H →
+ 'C_(|to)(A) / H = 'C_(|to / H)(A).

End ExternalAction.
@@ -336,24 +335,24 @@ Section SylowSolvableAct.

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

Lemma sol_coprime_Sylow_exists A G :
-    solvable A → A \subset 'N(G) → coprime #|G| #|A| →
-  exists2 P : {group gT}, p.-Sylow(G) P & A \subset 'N(P).
+    solvable A → A \subset 'N(G) → coprime #|G| #|A| →
+  exists2 P : {group gT}, p.-Sylow(G) P & A \subset 'N(P).

Lemma sol_coprime_Sylow_trans A G :
-    solvable A → A \subset 'N(G) → coprime #|G| #|A| →
-  [transitive 'C_G(A), on [set P in 'Syl_p(G) | A \subset 'N(P)] | 'JG].
+    solvable A → A \subset 'N(G) → coprime #|G| #|A| →
+  [transitive 'C_G(A), on [set P in 'Syl_p(G) | A \subset 'N(P)] | 'JG].

Lemma sol_coprime_Sylow_subset A G X :
-  A \subset 'N(G) → coprime #|G| #|A| → solvable A →
-  X \subset G → p.-group X → A \subset 'N(X) →
-  ∃ P : {group gT}, [/\ p.-Sylow(G) P, A \subset 'N(P) & X \subset P].
+  A \subset 'N(G) → coprime #|G| #|A| → solvable A →
+  X \subset G → p.-group X → A \subset 'N(X) →
+  ∃ P : {group gT}, [/\ p.-Sylow(G) P, A \subset 'N(P) & X \subset P].

End SylowSolvableAct.
-- cgit v1.2.3