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.jordanholder.html | 169 +++++++++++------------
1 file changed, 84 insertions(+), 85 deletions(-)
(limited to 'docs/htmldoc/mathcomp.solvable.jordanholder.html')
diff --git a/docs/htmldoc/mathcomp.solvable.jordanholder.html b/docs/htmldoc/mathcomp.solvable.jordanholder.html
index 267e1a4..a65d14f 100644
--- a/docs/htmldoc/mathcomp.solvable.jordanholder.html
+++ b/docs/htmldoc/mathcomp.solvable.jordanholder.html
@@ -21,7 +21,6 @@
@@ -85,48 +84,48 @@
Set Implicit Arguments.
-Inductive section (gT : finGroupType) := GSection of {group gT} × {group gT}.
+Inductive section (gT : finGroupType) := GSection of {group gT} × {group gT}.
Delimit Scope section_scope with sec.
-Definition mkSec (gT : finGroupType) (G1 G2 : {group gT}) := GSection (G1, G2).
+Definition mkSec (gT : finGroupType) (G1 G2 : {group gT}) := GSection (G1, G2).
-Infix "/" := mkSec : section_scope.
+Infix "/" := mkSec : section_scope.
Coercion pair_of_section gT (s : section gT) := let: GSection u := s in u.
-Coercion quotient_of_section gT (s : section gT) : GroupSet.sort _ := s.1 / s.2.
+Coercion quotient_of_section gT (s : section gT) : GroupSet.sort _ := s.1 / s.2.
-Coercion section_group gT (s : section gT) : {group (coset_of s.2)} :=
- Eval hnf in [group of s].
+Coercion section_group gT (s : section gT) : {group (coset_of s.2)} :=
+ Eval hnf in [group of s].
Section Sections.
Variables (gT : finGroupType).
-Implicit Types (G : {group gT}) (s : section gT).
+Implicit Types (G : {group gT}) (s : section gT).
-Canonical section_subType := Eval hnf in [newType for @pair_of_section gT].
-Definition section_eqMixin := Eval hnf in [eqMixin of section gT by <:].
+Canonical section_subType := Eval hnf in [newType for @pair_of_section gT].
+Definition section_eqMixin := Eval hnf in [eqMixin of section gT by <:].
Canonical section_eqType := Eval hnf in EqType (section gT) section_eqMixin.
-Definition section_choiceMixin := [choiceMixin of section gT by <:].
+Definition section_choiceMixin := [choiceMixin of section gT by <:].
Canonical section_choiceType :=
Eval hnf in ChoiceType (section gT) section_choiceMixin.
-Definition section_countMixin := [countMixin of section gT by <:].
+Definition section_countMixin := [countMixin of section gT by <:].
Canonical section_countType :=
Eval hnf in CountType (section gT) section_countMixin.
-Canonical section_subCountType := Eval hnf in [subCountType of section gT].
-Definition section_finMixin := [finMixin of section gT by <:].
+Canonical section_subCountType := Eval hnf in [subCountType of section gT].
+Definition section_finMixin := [finMixin of section gT by <:].
Canonical section_finType := Eval hnf in FinType (section gT) section_finMixin.
-Canonical section_subFinType := Eval hnf in [subFinType of section gT].
+Canonical section_subFinType := Eval hnf in [subFinType of section gT].
Canonical section_group.
@@ -138,7 +137,7 @@
@@ -147,20 +146,20 @@
A witness of the isomorphism class of a section
@@ -206,7 +205,7 @@
Lemma JordanHolderUniqueness (G : gTg) (s1 s2 : seq gTg) :
- comps G s1 → comps G s2 → perm_eq (mkfactors G s1) (mkfactors G s2).
+ comps G s1 → comps G s2 → perm_eq (mkfactors G s1) (mkfactors G s2).
End CompositionSeries.
@@ -224,24 +223,24 @@
Variables (aT rT : finGroupType).
-Variables (A : {group aT}) (D : {group rT}).
+Variables (A : {group aT}) (D : {group rT}).
Variable to : groupAction A D.
-Lemma gactsP (G : {set rT}) : reflect {acts A, on G | to} [acts A, on G | to].
+Lemma gactsP (G : {set rT}) : reflect {acts A, on G | to} [acts A, on G | to].
-Lemma gactsM (N1 N2 : {set rT}) :
- N1 \subset D → N2 \subset D →
- [acts A, on N1 | to] → [acts A, on N2 | to] → [acts A, on N1 × N2 | to].
+Lemma gactsM (N1 N2 : {set rT}) :
+ N1 \subset D → N2 \subset D →
+ [acts A, on N1 | to] → [acts A, on N2 | to] → [acts A, on N1 × N2 | to].
-Lemma gactsI (N1 N2 : {set rT}) :
- [acts A, on N1 | to] → [acts A, on N2 | to] → [acts A, on N1 :&: N2 | to].
+Lemma gactsI (N1 N2 : {set rT}) :
+ [acts A, on N1 | to] → [acts A, on N2 | to] → [acts A, on N1 :&: N2 | to].
-Lemma gastabsP (S : {set rT}) (a : aT) :
- a \in A → reflect (∀ x, (to x a \in S) = (x \in S)) (a \in 'N(S | to)).
+Lemma gastabsP (S : {set rT}) (a : aT) :
+ a \in A → reflect (∀ x, (to x a \in S) = (x \in S)) (a \in 'N(S | to)).
End MoreGroupAction.
@@ -259,26 +258,26 @@
Variables (aT rT : finGroupType).
-Variables (A : {group aT})(D : {group rT}).
+Variables (A : {group aT})(D : {group rT}).
Variable to : groupAction A D.
-Lemma qact_dom_doms (H : {group rT}) : H \subset D → qact_dom to H \subset A.
+Lemma qact_dom_doms (H : {group rT}) : H \subset D → qact_dom to H \subset A.
-Lemma acts_qact_doms (H : {group rT}) :
- H \subset D → [acts A, on H | to] → qact_dom to H :=: A.
+Lemma acts_qact_doms (H : {group rT}) :
+ H \subset D → [acts A, on H | to] → qact_dom to H :=: A.
-Lemma qacts_cosetpre (H : {group rT}) (K' : {group coset_of H}) :
- H \subset D → [acts A, on H | to] →
- [acts qact_dom to H, on K' | to / H] →
- [acts A, on coset H @*^-1 K' | to].
+Lemma qacts_cosetpre (H : {group rT}) (K' : {group coset_of H}) :
+ H \subset D → [acts A, on H | to] →
+ [acts qact_dom to H, on K' | to / H] →
+ [acts A, on coset H @*^-1 K' | to].
-Lemma qacts_coset (H K : {group rT}) :
- H \subset D → [acts A, on K | to] →
- [acts qact_dom to H, on (coset H) @* K | to / H].
+Lemma qacts_coset (H K : {group rT}) :
+ H \subset D → [acts A, on K | to] →
+ [acts qact_dom to H, on (coset H) @* K | to / H].
End MoreQuotientAction.
@@ -288,78 +287,78 @@
Variables (aT rT : finGroupType).
-Variables (D : {group rT})(A : {group aT}).
+Variables (D : {group rT})(A : {group aT}).
Variable to : groupAction A D.
-Definition maxainv (B C : {set rT}) :=
- [max C of H |
- [&& (H <| B), ~~ (B \subset H) & [acts A, on H | to]]].
+Definition maxainv (B C : {set rT}) :=
+ [max C of H |
+ [&& (H <| B), ~~ (B \subset H) & [acts A, on H | to]]].
Section MaxAinvProps.
-Variables K N : {group rT}.
+Variables K N : {group rT}.
-Lemma maxainv_norm : maxainv K N → N <| K.
+Lemma maxainv_norm : maxainv K N → N <| K.
-Lemma maxainv_proper : maxainv K N → N \proper K.
+Lemma maxainv_proper : maxainv K N → N \proper K.
-Lemma maxainv_sub : maxainv K N → N \subset K.
+Lemma maxainv_sub : maxainv K N → N \subset K.
-Lemma maxainv_ainvar : maxainv K N → A \subset 'N(N | to).
+Lemma maxainv_ainvar : maxainv K N → A \subset 'N(N | to).
-Lemma maxainvS : maxainv K N → N \subset K.
+Lemma maxainvS : maxainv K N → N \subset K.
-Lemma maxainv_exists : K :!=: 1 → {N : {group rT} | maxainv K N}.
+Lemma maxainv_exists : K :!=: 1 → {N : {group rT} | maxainv K N}.
End MaxAinvProps.
-Lemma maxainvM (G H K : {group rT}) :
- H \subset D → K \subset D → maxainv G H → maxainv G K →
- H :<>: K → H × K = G.
+Lemma maxainvM (G H K : {group rT}) :
+ H \subset D → K \subset D → maxainv G H → maxainv G K →
+ H :<>: K → H × K = G.
-Definition asimple (K : {set rT}) := maxainv K 1.
+Definition asimple (K : {set rT}) := maxainv K 1.
-Implicit Types (H K : {group rT}) (s : seq {group rT}).
+Implicit Types (H K : {group rT}) (s : seq {group rT}).
Lemma asimpleP K :
- reflect [/\ K :!=: 1
- & ∀ H, H <| K → [acts A, on H | to] → H :=: 1 ∨ H :=: K]
+ reflect [/\ K :!=: 1
+ & ∀ H, H <| K → [acts A, on H | to] → H :=: 1 ∨ H :=: K]
(asimple K).
Definition acomps K s :=
- ((last K s) == 1%G) && path [rel x y : {group rT} | maxainv x y] K s.
+ ((last K s) == 1%G) && path [rel x y : {group rT} | maxainv x y] K s.
Lemma acompsP K s :
- reflect (last K s = 1%G ∧ path [rel x y : {group rT} | maxainv x y] K s)
+ reflect (last K s = 1%G ∧ path [rel x y : {group rT} | maxainv x y] K s)
(acomps K s).
-Lemma trivg_acomps K s : acomps K s → (K :==: 1) = (s == [::]).
+Lemma trivg_acomps K s : acomps K s → (K :==: 1) = (s == [::]).
-Lemma acomps_cons K H s : acomps K (H :: s) → acomps H s.
+Lemma acomps_cons K H s : acomps K (H :: s) → acomps H s.
-Lemma asimple_acompsP K s : acomps K s → reflect (s = [:: 1%G]) (asimple K).
+Lemma asimple_acompsP K s : acomps K s → reflect (s = [:: 1%G]) (asimple K).
-Lemma exists_acomps K : ∃ s, acomps K s.
+Lemma exists_acomps K : ∃ s, acomps K s.
End StableCompositionSeries.
@@ -374,31 +373,31 @@
Variables aT rT : finGroupType.
-Variables (A : {group aT}) (D : {group rT}) (to : groupAction A D).
+Variables (A : {group aT}) (D : {group rT}) (to : groupAction A D).
-Lemma maxainv_asimple_quo (G H : {group rT}) :
- H \subset D → maxainv to G H → asimple (to / H) (G / H).
+Lemma maxainv_asimple_quo (G H : {group rT}) :
+ H \subset D → maxainv to G H → asimple (to / H) (G / H).
-Lemma asimple_quo_maxainv (G H : {group rT}) :
- H \subset D → G \subset D → [acts A, on G | to] → [acts A, on H | to] →
- H <| G → asimple (to / H) (G / H) →
+Lemma asimple_quo_maxainv (G H : {group rT}) :
+ H \subset D → G \subset D → [acts A, on G | to] → [acts A, on H | to] →
+ H <| G → asimple (to / H) (G / H) →
maxainv to G H.
-Lemma asimpleI (N1 N2 : {group rT}) :
- N2 \subset 'N(N1) → N1 \subset D →
- [acts A, on N1 | to] → [acts A, on N2 | to] →
- asimple (to / N1) (N2 / N1) →
- asimple (to / (N2 :&: N1)) (N2 / (N2 :&: N1)).
+Lemma asimpleI (N1 N2 : {group rT}) :
+ N2 \subset 'N(N1) → N1 \subset D →
+ [acts A, on N1 | to] → [acts A, on N2 | to] →
+ asimple (to / N1) (N2 / N1) →
+ asimple (to / (N2 :&: N1)) (N2 / (N2 :&: N1)).
End AuxiliaryLemmas.
Variables (aT rT : finGroupType).
-Variables (A : {group aT}) (D : {group rT}) (to : groupAction A D).
+Variables (A : {group aT}) (D : {group rT}) (to : groupAction A D).
@@ -410,8 +409,8 @@