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.gseries.html | 189 ++++++++++++++-------------- 1 file changed, 94 insertions(+), 95 deletions(-) (limited to 'docs/htmldoc/mathcomp.solvable.gseries.html') diff --git a/docs/htmldoc/mathcomp.solvable.gseries.html b/docs/htmldoc/mathcomp.solvable.gseries.html index 47341ea..d503193 100644 --- a/docs/htmldoc/mathcomp.solvable.gseries.html +++ b/docs/htmldoc/mathcomp.solvable.gseries.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.

@@ -62,68 +61,68 @@
Variable gT : finGroupType.
-Implicit Types A B U V : {set gT}.
+Implicit Types A B U V : {set gT}.


Definition subnormal A B :=
-  (A \subset B) && (iter #|B| (fun N ⇒ generated (class_support A N)) B == A).
+  (A \subset B) && (iter #|B| (fun N ⇒ generated (class_support A N)) B == A).

Definition invariant_factor A B C :=
-  [&& A \subset 'N(B), A \subset 'N(C) & B <| C].
+  [&& A \subset 'N(B), A \subset 'N(C) & B <| C].

-Definition group_rel_of (r : rel {set gT}) := [rel H G : groupT | r H G].
+Definition group_rel_of (r : rel {set gT}) := [rel H G : groupT | r H G].

Definition stable_factor A V U :=
-  ([~: U, A] \subset V) && (V <| U). (* this orders allows and3P to be used *)
+  ([~: U, A] \subset V) && (V <| U). (* this orders allows and3P to be used *)

Definition central_factor A V U :=
-  [&& [~: U, A] \subset V, V \subset U & U \subset A].
+  [&& [~: U, A] \subset V, V \subset U & U \subset A].

-Definition maximal A B := [max A of G | G \proper B].
+Definition maximal A B := [max A of G | G \proper B].

-Definition maximal_eq A B := (A == B) || maximal A B.
+Definition maximal_eq A B := (A == B) || maximal A B.

-Definition maxnormal A B U := [max A of G | G \proper B & U \subset 'N(G)].
+Definition maxnormal A B U := [max A of G | G \proper B & U \subset 'N(G)].

-Definition minnormal A B := [min A of G | G :!=: 1 & B \subset 'N(G)].
+Definition minnormal A B := [min A of G | G :!=: 1 & B \subset 'N(G)].

Definition simple A := minnormal A A.

-Definition chief_factor A V U := maxnormal V U A && (U <| A).
+Definition chief_factor A V U := maxnormal V U A && (U <| A).
End GroupDefs.


-Notation "H <|<| G" := (subnormal H G)
+Notation "H <|<| G" := (subnormal H G)
  (at level 70, no associativity) : group_scope.

-Notation "A .-invariant" := (invariant_factor A)
+Notation "A .-invariant" := (invariant_factor A)
  (at level 2, format "A .-invariant") : group_rel_scope.
-Notation "A .-stable" := (stable_factor A)
+Notation "A .-stable" := (stable_factor A)
  (at level 2, format "A .-stable") : group_rel_scope.
-Notation "A .-central" := (central_factor A)
+Notation "A .-central" := (central_factor A)
  (at level 2, format "A .-central") : group_rel_scope.
-Notation "G .-chief" := (chief_factor G)
+Notation "G .-chief" := (chief_factor G)
  (at level 2, format "G .-chief") : group_rel_scope.


-Notation "r .-series" := (path (rel_of_simpl_rel (group_rel_of r)))
+Notation "r .-series" := (path (rel_of_simpl_rel (group_rel_of r)))
  (at level 2, format "r .-series") : group_scope.

@@ -131,51 +130,51 @@
Variable gT : finGroupType.
-Implicit Types (A B C D : {set gT}) (G H K : {group gT}).
+Implicit Types (A B C D : {set gT}) (G H K : {group gT}).

-Let setIgr H G := (G :&: H)%G.
-Let sub_setIgr G H : G \subset H → G = setIgr H G.
+Let setIgr H G := (G :&: H)%G.
+Let sub_setIgr G H : G \subset H → G = setIgr H G.

Let path_setIgr H G s :
-   normal.-series H s → normal.-series (setIgr G H) (map (setIgr G) s).
+   normal.-series H s → normal.-series (setIgr G H) (map (setIgr G) s).

Lemma subnormalP H G :
-  reflect (exists2 s, normal.-series H s & last H s = G) (H <|<| G).
+  reflect (exists2 s, normal.-series H s & last H s = G) (H <|<| G).

-Lemma subnormal_refl G : G <|<| G.
+Lemma subnormal_refl G : G <|<| G.

-Lemma subnormal_trans K H G : H <|<| K → K <|<| G → H <|<| G.
+Lemma subnormal_trans K H G : H <|<| K → K <|<| G → H <|<| G.

-Lemma normal_subnormal H G : H <| G → H <|<| G.
+Lemma normal_subnormal H G : H <| G → H <|<| G.

-Lemma setI_subnormal G H K : K \subset G → H <|<| G → H :&: K <|<| K.
+Lemma setI_subnormal G H K : K \subset G → H <|<| G → H :&: K <|<| K.

-Lemma subnormal_sub G H : H <|<| G → H \subset G.
+Lemma subnormal_sub G H : H <|<| G → H \subset G.

Lemma invariant_subnormal A G H :
-    A \subset 'N(G) → A \subset 'N(H) → H <|<| G →
-  exists2 s, (A.-invariant).-series H s & last H s = G.
+    A \subset 'N(G) → A \subset 'N(H) → H <|<| G →
+  exists2 s, (A.-invariant).-series H s & last H s = G.

Lemma subnormalEsupport G H :
-  H <|<| G → H :=: G ∨ <<class_support H G>> \proper G.
+  H <|<| G → H :=: G ∨ <<class_support H G>> \proper G.

-Lemma subnormalEr G H : H <|<| G →
-  H :=: G ∨ (∃ K : {group gT}, [/\ H <|<| K, K <| G & K \proper G]).
+Lemma subnormalEr G H : H <|<| G →
+  H :=: G ∨ (∃ K : {group gT}, [/\ H <|<| K, K <| G & K \proper G]).

-Lemma subnormalEl G H : H <|<| G →
-  H :=: G ∨ (∃ K : {group gT}, [/\ H <| K, K <|<| G & H \proper K]).
+Lemma subnormalEl G H : H <|<| G →
+  H :=: G ∨ (∃ K : {group gT}, [/\ H <| K, K <|<| G & H \proper K]).

End Subnormal.
@@ -187,14 +186,14 @@
Variable gT : finGroupType.
-Implicit Type G H K : {group gT}.
+Implicit Type G H K : {group gT}.

-Lemma morphim_subnormal (rT : finGroupType) G (f : {morphism G >-> rT}) H K :
-  H <|<| K → f @* H <|<| f @* K.
+Lemma morphim_subnormal (rT : finGroupType) G (f : {morphism G >-> rT}) H K :
+  H <|<| K → f @* H <|<| f @* K.

-Lemma quotient_subnormal H G K : G <|<| K → G / H <|<| K / H.
+Lemma quotient_subnormal H G K : G <|<| K → G / H <|<| K / H.

End MorphSubNormal.
@@ -204,22 +203,22 @@
Variable gT : finGroupType.
-Implicit Types G H M : {group gT}.
+Implicit Types G H M : {group gT}.

Lemma maximal_eqP M G :
-  reflect (M \subset G ∧
-             ∀ H, M \subset H → H \subset G → H :=: M ∨ H :=: G)
+  reflect (M \subset G ∧
+             ∀ H, M \subset H → H \subset G → H :=: M ∨ H :=: G)
       (maximal_eq M G).

Lemma maximal_exists H G :
-    H \subset G →
-  H :=: G ∨ (exists2 M : {group gT}, maximal M G & H \subset M).
+    H \subset G →
+  H :=: G ∨ (exists2 M : {group gT}, maximal M G & H \subset M).

Lemma mulg_normal_maximal G M H :
-  M <| G → maximal M G → H \subset G → ~~ (H \subset M) → (M × H = G)%g.
+  M <| G → maximal M G → H \subset G → ~~ (H \subset M) → (M × H = G)%g.

End MaxProps.
@@ -229,11 +228,11 @@
Variable gT : finGroupType.
-Implicit Types G H M : {group gT}.
+Implicit Types G H M : {group gT}.

-Lemma minnormal_exists G H : H :!=: 1 → G \subset 'N(H) →
-  {M : {group gT} | minnormal M G & M \subset H}.
+Lemma minnormal_exists G H : H :!=: 1 → G \subset 'N(H) →
+  {M : {group gT} | minnormal M G & M \subset H}.

End MinProps.
@@ -242,15 +241,15 @@ Section MorphPreMax.

-Variables (gT rT : finGroupType) (D : {group gT}) (f : {morphism D >-> rT}).
-Variables (M G : {group rT}).
-Hypotheses (dM : M \subset f @* D) (dG : G \subset f @* D).
+Variables (gT rT : finGroupType) (D : {group gT}) (f : {morphism D >-> rT}).
+Variables (M G : {group rT}).
+Hypotheses (dM : M \subset f @* D) (dG : G \subset f @* D).

-Lemma morphpre_maximal : maximal (f @*^-1 M) (f @*^-1 G) = maximal M G.
+Lemma morphpre_maximal : maximal (f @*^-1 M) (f @*^-1 G) = maximal M G.

-Lemma morphpre_maximal_eq : maximal_eq (f @*^-1 M) (f @*^-1 G) = maximal_eq M G.
+Lemma morphpre_maximal_eq : maximal_eq (f @*^-1 M) (f @*^-1 G) = maximal_eq M G.

End MorphPreMax.
@@ -259,24 +258,24 @@ Section InjmMax.

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

-Hypothesis injf : 'injm f.
-Hypotheses (dM : M \subset D) (dG : G \subset D) (dL : L \subset D).
+Hypothesis injf : 'injm f.
+Hypotheses (dM : M \subset D) (dG : G \subset D) (dL : L \subset D).

-Lemma injm_maximal : maximal (f @* M) (f @* G) = maximal M G.
+Lemma injm_maximal : maximal (f @* M) (f @* G) = maximal M G.

-Lemma injm_maximal_eq : maximal_eq (f @* M) (f @* G) = maximal_eq M G.
+Lemma injm_maximal_eq : maximal_eq (f @* M) (f @* G) = maximal_eq M G.

-Lemma injm_maxnormal : maxnormal (f @* M) (f @* G) (f @* L) = maxnormal M G L.
+Lemma injm_maxnormal : maxnormal (f @* M) (f @* G) (f @* L) = maxnormal M G L.

-Lemma injm_minnormal : minnormal (f @* M) (f @* G) = minnormal M G.
+Lemma injm_minnormal : minnormal (f @* M) (f @* G) = minnormal M G.

End InjmMax.
@@ -285,29 +284,29 @@ Section QuoMax.

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

-Lemma cosetpre_maximal (Q R : {group coset_of K}) :
-  maximal (coset K @*^-1 Q) (coset K @*^-1 R) = maximal Q R.
+Lemma cosetpre_maximal (Q R : {group coset_of K}) :
+  maximal (coset K @*^-1 Q) (coset K @*^-1 R) = maximal Q R.

-Lemma cosetpre_maximal_eq (Q R : {group coset_of K}) :
-  maximal_eq (coset K @*^-1 Q) (coset K @*^-1 R) = maximal_eq Q R.
+Lemma cosetpre_maximal_eq (Q R : {group coset_of K}) :
+  maximal_eq (coset K @*^-1 Q) (coset K @*^-1 R) = maximal_eq Q R.

Lemma quotient_maximal :
-  K <| G → K <| H → maximal (G / K) (H / K) = maximal G H.
+  K <| G → K <| H → maximal (G / K) (H / K) = maximal G H.

Lemma quotient_maximal_eq :
-  K <| G → K <| H → maximal_eq (G / K) (H / K) = maximal_eq G H.
+  K <| G → K <| H → maximal_eq (G / K) (H / K) = maximal_eq G H.

-Lemma maximalJ x : maximal (G :^ x) (H :^ x) = maximal G H.
+Lemma maximalJ x : maximal (G :^ x) (H :^ x) = maximal G H.

-Lemma maximal_eqJ x : maximal_eq (G :^ x) (H :^ x) = maximal_eq G H.
+Lemma maximal_eqJ x : maximal_eq (G :^ x) (H :^ x) = maximal_eq G H.

End QuoMax.
@@ -317,32 +316,32 @@
Variables (gT : finGroupType).
-Implicit Types (A B C : {set gT}) (G H K L M : {group gT}).
+Implicit Types (A B C : {set gT}) (G H K L M : {group gT}).

-Lemma maxnormal_normal A B : maxnormal A B B → A <| B.
+Lemma maxnormal_normal A B : maxnormal A B B → A <| B.

-Lemma maxnormal_proper A B C : maxnormal A B C → A \proper B.
+Lemma maxnormal_proper A B C : maxnormal A B C → A \proper B.

-Lemma maxnormal_sub A B C : maxnormal A B C → A \subset B.
+Lemma maxnormal_sub A B C : maxnormal A B C → A \subset B.

-Lemma ex_maxnormal_ntrivg G : G :!=: 1→ {N : {group gT} | maxnormal N G G}.
+Lemma ex_maxnormal_ntrivg G : G :!=: 1→ {N : {group gT} | maxnormal N G G}.

Lemma maxnormalM G H K :
-  maxnormal H G G → maxnormal K G G → H :<>: K → H × K = G.
+  maxnormal H G G → maxnormal K G G → H :<>: K → H × K = G.

Lemma maxnormal_minnormal G L M :
-    G \subset 'N(M) → L \subset 'N(G) → maxnormal M G L →
-  minnormal (G / M) (L / M).
+    G \subset 'N(M) → L \subset 'N(G) → maxnormal M G L →
+  minnormal (G / M) (L / M).

Lemma minnormal_maxnormal G L M :
-  M <| G → L \subset 'N(M) → minnormal (G / M) (L / M) → maxnormal M G L.
+  M <| G → L \subset 'N(M) → minnormal (G / M) (L / M) → maxnormal M G L.

End MaxNormalProps.
@@ -354,20 +353,20 @@ Implicit Types gT rT : finGroupType.

-Lemma simpleP gT (G : {group gT}) :
-  reflect (G :!=: 1 ∧ ∀ H : {group gT}, H <| G → H :=: 1 ∨ H :=: G)
+Lemma simpleP gT (G : {group gT}) :
+  reflect (G :!=: 1 ∧ ∀ H : {group gT}, H <| G → H :=: 1 ∨ H :=: G)
          (simple G).

-Lemma quotient_simple gT (G H : {group gT}) :
-  H <| G → simple (G / H) = maxnormal H G G.
+Lemma quotient_simple gT (G H : {group gT}) :
+  H <| G → simple (G / H) = maxnormal H G G.

-Lemma isog_simple gT rT (G : {group gT}) (M : {group rT}) :
-  G \isog M → simple G = simple M.
+Lemma isog_simple gT rT (G : {group gT}) (M : {group rT}) :
+  G \isog M → simple G = simple M.

-Lemma simple_maxnormal gT (G : {group gT}) : simple G = maxnormal 1 G G.
+Lemma simple_maxnormal gT (G : {group gT}) : simple G = maxnormal 1 G G.

End Simple.
@@ -377,20 +376,20 @@
Variable gT : finGroupType.
-Implicit Types G H U V : {group gT}.
+Implicit Types G H U V : {group gT}.

Lemma chief_factor_minnormal G V U :
-  chief_factor G V U → minnormal (U / V) (G / V).
+  chief_factor G V U → minnormal (U / V) (G / V).

Lemma acts_irrQ G U V :
-    G \subset 'N(V) → V <| U →
-  acts_irreducibly G (U / V) 'Q = minnormal (U / V) (G / V).
+    G \subset 'N(V) → V <| U →
+  acts_irreducibly G (U / V) 'Q = minnormal (U / V) (G / V).

Lemma chief_series_exists H G :
-  H <| G → {s | (G.-chief).-series 1%G s & last 1%G s = H}.
+  H <| G → {s | (G.-chief).-series 1%G s & last 1%G s = H}.

End Chiefs.
@@ -399,16 +398,16 @@ Section Central.

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

Lemma central_factor_central H K :
-  central_factor G H K → (K / H) \subset 'Z(G / H).
+  central_factor G H K → (K / H) \subset 'Z(G / H).

Lemma central_central_factor H K :
-  (K / H) \subset 'Z(G / H) → H <| K → H <| G → central_factor G H K.
+  (K / H) \subset 'Z(G / H) → H <| K → H <| G → central_factor G H K.

End Central.
-- cgit v1.2.3