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.sylow.html | 165 +++++++++++++++--------------- 1 file changed, 82 insertions(+), 83 deletions(-) (limited to 'docs/htmldoc/mathcomp.solvable.sylow.html') diff --git a/docs/htmldoc/mathcomp.solvable.sylow.html b/docs/htmldoc/mathcomp.solvable.sylow.html index 151cabb..0ec7af3 100644 --- a/docs/htmldoc/mathcomp.solvable.sylow.html +++ b/docs/htmldoc/mathcomp.solvable.sylow.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.

@@ -50,12 +49,12 @@ Section ModP.

-Variable (aT : finGroupType) (sT : finType) (D : {group aT}).
+Variable (aT : finGroupType) (sT : finType) (D : {group aT}).
Variable to : action D sT.

-Lemma pgroup_fix_mod (p : nat) (G : {group aT}) (S : {set sT}) :
-  p.-group G → [acts G, on S | to] → #|S| = #|'Fix_(S | to)(G)| %[mod p].
+Lemma pgroup_fix_mod (p : nat) (G : {group aT}) (S : {set sT}) :
+  p.-group G → [acts G, on S | to] → #|S| = #|'Fix_(S | to)(G)| %[mod p].

End ModP.
@@ -64,25 +63,25 @@ Section ModularGroupAction.

-Variables (aT rT : finGroupType) (D : {group aT}) (R : {group rT}).
-Variables (to : groupAction D R) (p : nat).
-Implicit Types (G H : {group aT}) (M : {group rT}).
+Variables (aT rT : finGroupType) (D : {group aT}) (R : {group rT}).
+Variables (to : groupAction D R) (p : nat).
+Implicit Types (G H : {group aT}) (M : {group rT}).

Lemma nontrivial_gacent_pgroup G M :
-    p.-group G → p.-group M → {acts G, on group M | to} →
-  M :!=: 1 → 'C_(M | to)(G) :!=: 1.
+    p.-group G → p.-group M → {acts G, on group M | to} →
+  M :!=: 1 → 'C_(M | to)(G) :!=: 1.

Lemma pcore_sub_astab_irr G M :
-    p.-group M → M \subset R → acts_irreducibly G M to →
-  'O_p(G) \subset 'C_G(M | to).
+    p.-group M → M \subset R → acts_irreducibly G M to →
+  'O_p(G) \subset 'C_G(M | to).

Lemma pcore_faithful_irr_act G M :
-    p.-group M → M \subset R → acts_irreducibly G M to →
-    [faithful G, on M | to] →
-  'O_p(G) = 1.
+    p.-group M → M \subset R → acts_irreducibly G M to →
+    [faithful G, on M | to] →
+  'O_p(G) = 1.

End ModularGroupAction.
@@ -91,54 +90,54 @@ Section Sylow.

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

Theorem Sylow's_theorem :
-  [/\ ∀ P, [max P | p.-subgroup(G) P] = p.-Sylow(G) P,
-      [transitive G, on 'Syl_p(G) | 'JG],
-      ∀ P, p.-Sylow(G) P → #|'Syl_p(G)| = #|G : 'N_G(P)|
-   & prime p → #|'Syl_p(G)| %% p = 1%N].
+  [/\ ∀ P, [max P | p.-subgroup(G) P] = p.-Sylow(G) P,
+      [transitive G, on 'Syl_p(G) | 'JG],
+      ∀ P, p.-Sylow(G) P → #|'Syl_p(G)| = #|G : 'N_G(P)|
+   & prime p → #|'Syl_p(G)| %% p = 1%N].

-Lemma max_pgroup_Sylow P : [max P | p.-subgroup(G) P] = p.-Sylow(G) P.
+Lemma max_pgroup_Sylow P : [max P | p.-subgroup(G) P] = p.-Sylow(G) P.

Lemma Sylow_superset Q :
-  Q \subset G → p.-group Q → {P : {group gT} | p.-Sylow(G) P & Q \subset P}.
+  Q \subset G → p.-group Q → {P : {group gT} | p.-Sylow(G) P & Q \subset P}.

-Lemma Sylow_exists : {P : {group gT} | p.-Sylow(G) P}.
+Lemma Sylow_exists : {P : {group gT} | p.-Sylow(G) P}.

-Lemma Syl_trans : [transitive G, on 'Syl_p(G) | 'JG].
+Lemma Syl_trans : [transitive G, on 'Syl_p(G) | 'JG].

Lemma Sylow_trans P Q :
-  p.-Sylow(G) P → p.-Sylow(G) Q → exists2 x, x \in G & Q :=: P :^ x.
+  p.-Sylow(G) P → p.-Sylow(G) Q → exists2 x, x \in G & Q :=: P :^ x.

Lemma Sylow_subJ P Q :
-    p.-Sylow(G) P → Q \subset G → p.-group Q →
-  exists2 x, x \in G & Q \subset P :^ x.
+    p.-Sylow(G) P → Q \subset G → p.-group Q →
+  exists2 x, x \in G & Q \subset P :^ x.

Lemma Sylow_Jsub P Q :
-    p.-Sylow(G) P → Q \subset G → p.-group Q →
-  exists2 x, x \in G & Q :^ x \subset P.
+    p.-Sylow(G) P → Q \subset G → p.-group Q →
+  exists2 x, x \in G & Q :^ x \subset P.

-Lemma card_Syl P : p.-Sylow(G) P → #|'Syl_p(G)| = #|G : 'N_G(P)|.
+Lemma card_Syl P : p.-Sylow(G) P → #|'Syl_p(G)| = #|G : 'N_G(P)|.

-Lemma card_Syl_dvd : #|'Syl_p(G)| %| #|G|.
+Lemma card_Syl_dvd : #|'Syl_p(G)| %| #|G|.

-Lemma card_Syl_mod : prime p → #|'Syl_p(G)| %% p = 1%N.
+Lemma card_Syl_mod : prime p → #|'Syl_p(G)| %% p = 1%N.

-Lemma Frattini_arg H P : G <| H → p.-Sylow(G) P → G × 'N_H(P) = H.
+Lemma Frattini_arg H P : G <| H → p.-Sylow(G) P → G × 'N_H(P) = H.

End Sylow.
@@ -147,35 +146,35 @@ Section MoreSylow.

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

Lemma Sylow_setI_normal G H P :
-  G <| H → p.-Sylow(H) P → p.-Sylow(G) (G :&: P).
+  G <| H → p.-Sylow(H) P → p.-Sylow(G) (G :&: P).

Lemma normal_sylowP G :
-  reflect (exists2 P : {group gT}, p.-Sylow(G) P & P <| G)
-          (#|'Syl_p(G)| == 1%N).
+  reflect (exists2 P : {group gT}, p.-Sylow(G) P & P <| G)
+          (#|'Syl_p(G)| == 1%N).

-Lemma trivg_center_pgroup P : p.-group P → 'Z(P) = 1 → P :=: 1.
+Lemma trivg_center_pgroup P : p.-group P → 'Z(P) = 1 → P :=: 1.

-Lemma p2group_abelian P : p.-group P → logn p #|P| ≤ 2 → abelian P.
+Lemma p2group_abelian P : p.-group P → logn p #|P| ≤ 2 → abelian P.

-Lemma card_p2group_abelian P : prime p → #|P| = (p ^ 2)%N → abelian P.
+Lemma card_p2group_abelian P : prime p → #|P| = (p ^ 2)%N → abelian P.

-Lemma Sylow_transversal_gen (T : {set {group gT}}) G :
-    (∀ P, P \in T → P \subset G) →
-    (∀ p, p \in \pi(G) → exists2 P, P \in T & p.-Sylow(G) P) →
-  << \bigcup_(P in T) P >> = G.
+Lemma Sylow_transversal_gen (T : {set {group gT}}) G :
+    (∀ P, P \in T → P \subset G) →
+    (∀ p, p \in \pi(G) → exists2 P, P \in T & p.-Sylow(G) P) →
+  << \bigcup_(P in T) P >> = G.

-Lemma Sylow_gen G : <<\bigcup_(P : {group gT} | Sylow G P) P>> = G.
+Lemma Sylow_gen G : <<\bigcup_(P : {group gT} | Sylow G P) P>> = G.

End MoreSylow.
@@ -185,26 +184,26 @@
Variable gT : finGroupType.
-Implicit Types (p : nat) (pi : nat_pred) (G H K P R : {group gT}).
+Implicit Types (p : nat) (pi : nat_pred) (G H K P R : {group gT}).

Lemma Hall_pJsub p pi G H P :
-    pi.-Hall(G) H → p \in pi → P \subset G → p.-group P →
-  exists2 x, x \in G & P :^ x \subset H.
+    pi.-Hall(G) H → p \in pi → P \subset G → p.-group P →
+  exists2 x, x \in G & P :^ x \subset H.

Lemma Hall_psubJ p pi G H P :
-    pi.-Hall(G) H → p \in pi → P \subset G → p.-group P →
-  exists2 x, x \in G & P \subset H :^ x.
+    pi.-Hall(G) H → p \in pi → P \subset G → p.-group P →
+  exists2 x, x \in G & P \subset H :^ x.

Lemma Hall_setI_normal pi G K H :
-  K <| G → pi.-Hall(G) H → pi.-Hall(K) (H :&: K).
+  K <| G → pi.-Hall(G) H → pi.-Hall(K) (H :&: K).

Lemma coprime_mulG_setI_norm H G K R :
-    K × R = G → G \subset 'N(H) → coprime #|K| #|R| →
-  (K :&: H) × (R :&: H) = G :&: H.
+    K × R = G → G \subset 'N(H) → coprime #|K| #|R| →
+  (K :&: H) × (R :&: H) = G :&: H.

End SomeHall.
@@ -214,74 +213,74 @@
Variable gT : finGroupType.
-Implicit Types (G H K P L : {group gT}) (p q : nat).
+Implicit Types (G H K P L : {group gT}) (p q : nat).

-Lemma pgroup_nil p P : p.-group P → nilpotent P.
+Lemma pgroup_nil p P : p.-group P → nilpotent P.

-Lemma pgroup_sol p P : p.-group P → solvable P.
+Lemma pgroup_sol p P : p.-group P → solvable P.

-Lemma small_nil_class G : nil_class G ≤ 5 → nilpotent G.
+Lemma small_nil_class G : nil_class G ≤ 5 → nilpotent G.

-Lemma nil_class2 G : (nil_class G ≤ 2) = (G^`(1) \subset 'Z(G)).
+Lemma nil_class2 G : (nil_class G ≤ 2) = (G^`(1) \subset 'Z(G)).

-Lemma nil_class3 G : (nil_class G ≤ 3) = ('L_3(G) \subset 'Z(G)).
+Lemma nil_class3 G : (nil_class G ≤ 3) = ('L_3(G) \subset 'Z(G)).

Lemma nilpotent_maxp_normal pi G H :
-  nilpotent G → [max H | pi.-subgroup(G) H] → H <| G.
+  nilpotent G → [max H | pi.-subgroup(G) H] → H <| G.

Lemma nilpotent_Hall_pcore pi G H :
-  nilpotent G → pi.-Hall(G) H → H :=: 'O_pi(G).
+  nilpotent G → pi.-Hall(G) H → H :=: 'O_pi(G).

-Lemma nilpotent_pcore_Hall pi G : nilpotent G → pi.-Hall(G) 'O_pi(G).
+Lemma nilpotent_pcore_Hall pi G : nilpotent G → pi.-Hall(G) 'O_pi(G).

-Lemma nilpotent_pcoreC pi G : nilpotent G → 'O_pi(G) \x 'O_pi^'(G) = G.
+Lemma nilpotent_pcoreC pi G : nilpotent G → 'O_pi(G) \x 'O_pi^'(G) = G.

Lemma sub_nilpotent_cent2 H K G :
-    nilpotent G → K \subset G → H \subset G → coprime #|K| #|H| →
-  H \subset 'C(K).
+    nilpotent G → K \subset G → H \subset G → coprime #|K| #|H| →
+  H \subset 'C(K).

-Lemma pi_center_nilpotent G : nilpotent G → \pi('Z(G)) = \pi(G).
+Lemma pi_center_nilpotent G : nilpotent G → \pi('Z(G)) = \pi(G).

-Lemma Sylow_subnorm p G P : p.-Sylow('N_G(P)) P = p.-Sylow(G) P.
+Lemma Sylow_subnorm p G P : p.-Sylow('N_G(P)) P = p.-Sylow(G) P.

End Nilpotent.

-Lemma nil_class_pgroup (gT : finGroupType) (p : nat) (P : {group gT}) :
-  p.-group P → nil_class P ≤ maxn 1 (logn p #|P|).-1.
+Lemma nil_class_pgroup (gT : finGroupType) (p : nat) (P : {group gT}) :
+  p.-group P → nil_class P ≤ maxn 1 (logn p #|P|).-1.

-Definition Zgroup (gT : finGroupType) (A : {set gT}) :=
-  [∀ (V : {group gT} | Sylow A V), cyclic V].
+Definition Zgroup (gT : finGroupType) (A : {set gT}) :=
+  [∀ (V : {group gT} | Sylow A V), cyclic V].

Section Zgroups.

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

-Lemma ZgroupS G H : H \subset G → Zgroup G → Zgroup H.
+Lemma ZgroupS G H : H \subset G → Zgroup G → Zgroup H.

-Lemma morphim_Zgroup G : Zgroup G → Zgroup (f @* G).
+Lemma morphim_Zgroup G : Zgroup G → Zgroup (f @* G).

-Lemma nil_Zgroup_cyclic G : Zgroup G → nilpotent G → cyclic G.
+Lemma nil_Zgroup_cyclic G : Zgroup G → nilpotent G → cyclic G.

End Zgroups.
@@ -292,8 +291,8 @@ Section NilPGroups.

-Variables (p : nat) (gT : finGroupType).
-Implicit Type G P N : {group gT}.
+Variables (p : nat) (gT : finGroupType).
+Implicit Type G P N : {group gT}.

@@ -303,13 +302,13 @@
Lemma normal_pgroup r P N :
-    p.-group P → N <| P → r ≤ logn p #|N| →
-  ∃ Q : {group gT}, [/\ Q \subset N, Q <| P & #|Q| = (p ^ r)%N].
+    p.-group P → N <| P → r ≤ logn p #|N| →
+  ∃ Q : {group gT}, [/\ Q \subset N, Q <| P & #|Q| = (p ^ r)%N].

Theorem Baer_Suzuki x G :
-    x \in G → (∀ y, y \in G → p.-group <<[set x; x ^ y]>>) →
-  x \in 'O_p(G).
+    x \in G → (∀ y, y \in G → p.-group <<[set x; x ^ y]>>) →
+  x \in 'O_p(G).

End NilPGroups.
-- cgit v1.2.3