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.fingroup.quotient.html | 461 +++++++++++++--------------
1 file changed, 230 insertions(+), 231 deletions(-)
(limited to 'docs/htmldoc/mathcomp.fingroup.quotient.html')
diff --git a/docs/htmldoc/mathcomp.fingroup.quotient.html b/docs/htmldoc/mathcomp.fingroup.quotient.html
index 6e5d246..b2bdd94 100644
--- a/docs/htmldoc/mathcomp.fingroup.quotient.html
+++ b/docs/htmldoc/mathcomp.fingroup.quotient.html
@@ -21,7 +21,6 @@
@@ -52,7 +51,7 @@
Section Cosets.
-Variables (gT : finGroupType) (Q A : {set gT}).
+Variables (gT : finGroupType) (Q A : {set gT}).
@@ -82,25 +81,25 @@
@@ -119,25 +118,25 @@
Let nNH := subsetP (norm_gen A).
-Lemma coset_range_mul (B C : coset_of) : coset_range (B × C).
+Lemma coset_range_mul (B C : coset_of) : coset_range (B × C).
Definition coset_mul B C := Coset (coset_range_mul B C).
-Lemma coset_range_inv (B : coset_of) : coset_range B^-1.
+Lemma coset_range_inv (B : coset_of) : coset_range B^-1.
Definition coset_inv B := Coset (coset_range_inv B).
-Lemma coset_mulP : associative coset_mul.
+Lemma coset_mulP : associative coset_mul.
-Lemma coset_oneP : left_id coset_one coset_mul.
+Lemma coset_oneP : left_id coset_one coset_mul.
-Lemma coset_invP : left_inverse coset_one coset_inv coset_mul.
+Lemma coset_invP : left_inverse coset_one coset_inv coset_mul.
Definition coset_of_groupMixin :=
@@ -157,7 +156,7 @@
@@ -167,22 +166,22 @@
the case where A is a group.
@@ -193,13 +192,13 @@
@@ -209,26 +208,26 @@
guarantee repr xbar \in 'N(A) when A is a group.
@@ -307,7 +306,7 @@
Variant of morph1; no specialization for other morph lemmas.
@@ -316,7 +315,7 @@
Variant of kerE.
@@ -326,10 +325,10 @@
morph[im|pre]Iim are also covered by im_quotient.
@@ -338,110 +337,110 @@
Variant of morphimIdom.
@@ -450,32 +449,32 @@
Variant of morhphim_ker
@@ -484,156 +483,156 @@
Variant of ker_trivg_morphim.
-
Lemma quotient_sub1 A :
A \subset 'N(H) → (A / H \subset [1]) = (A \subset H).
+
Lemma quotient_sub1 A :
A \subset 'N(H) → (A / H \subset [1]) = (A \subset H).
Lemma quotientSK A B :
-
A \subset 'N(H) → (A / H \subset B / H) = (A \subset H × B).
+
A \subset 'N(H) → (A / H \subset B / H) = (A \subset H × B).
Lemma quotientSGK A G :
-
A \subset 'N(H) → H \subset G → (A / H \subset G / H) = (A \subset G).
+
A \subset 'N(H) → H \subset G → (A / H \subset G / H) = (A \subset G).
Lemma quotient_injG :
-
{in [pred G : {group gT} | H <| G] &, injective (
fun G ⇒
G / H)
}.
+
{in [pred G : {group gT} | H <| G] &, injective (
fun G ⇒
G / H)
}.
Lemma quotient_inj G1 G2 :
-
H <| G1 → H <| G2 → G1 / H = G2 / H → G1 :=: G2.
+
H <| G1 → H <| G2 → G1 / H = G2 / H → G1 :=: G2.
-
Lemma quotient_neq1 A :
H <| A → (A / H != 1
) = (H \proper A).
+
Lemma quotient_neq1 A :
H <| A → (A / H != 1
) = (H \proper A).
-
Lemma quotient_gen A :
A \subset 'N(H) → <<A>> / H = <<A / H>>.
+
Lemma quotient_gen A :
A \subset 'N(H) → <<A>> / H = <<A / H>>.
Lemma cosetpre_gen C :
- 1
\in C → coset H @*^-1 <<C>> = <<coset H @*^-1 C>>.
+ 1
\in C → coset H @*^-1 <<C>> = <<coset H @*^-1 C>>.
Lemma quotientR A B :
-
A \subset 'N(H) → B \subset 'N(H) → [~: A, B] / H = [~: A / H, B / H].
+
A \subset 'N(H) → B \subset 'N(H) → [~: A, B] / H = [~: A / H, B / H].
-
Lemma quotient_norm A :
'N(A) / H \subset 'N(A / H).
+
Lemma quotient_norm A :
'N(A) / H \subset 'N(A / H).
-
Lemma quotient_norms A B :
A \subset 'N(B) → A / H \subset 'N(B / H).
+
Lemma quotient_norms A B :
A \subset 'N(B) → A / H \subset 'N(B / H).
-
Lemma quotient_subnorm A B :
'N_A(B) / H \subset 'N_(A / H)(B / H).
+
Lemma quotient_subnorm A B :
'N_A(B) / H \subset 'N_(A / H)(B / H).
-
Lemma quotient_normal A B :
A <| B → A / H <| B / H.
+
Lemma quotient_normal A B :
A <| B → A / H <| B / H.
-
Lemma quotient_cent1 x :
'C[x] / H \subset 'C[coset H x].
+
Lemma quotient_cent1 x :
'C[x] / H \subset 'C[coset H x].
-
Lemma quotient_cent1s A x :
A \subset 'C[x] → A / H \subset 'C[coset H x].
+
Lemma quotient_cent1s A x :
A \subset 'C[x] → A / H \subset 'C[coset H x].
-
Lemma quotient_subcent1 A x :
'C_A[x] / H \subset 'C_(A / H)[coset H x].
+
Lemma quotient_subcent1 A x :
'C_A[x] / H \subset 'C_(A / H)[coset H x].
-
Lemma quotient_cent A :
'C(A) / H \subset 'C(A / H).
+
Lemma quotient_cent A :
'C(A) / H \subset 'C(A / H).
-
Lemma quotient_cents A B :
A \subset 'C(B) → A / H \subset 'C(B / H).
+
Lemma quotient_cents A B :
A \subset 'C(B) → A / H \subset 'C(B / H).
-
Lemma quotient_abelian A :
abelian A → abelian (
A / H).
+
Lemma quotient_abelian A :
abelian A → abelian (
A / H).
-
Lemma quotient_subcent A B :
'C_A(B) / H \subset 'C_(A / H)(B / H).
+
Lemma quotient_subcent A B :
'C_A(B) / H \subset 'C_(A / H)(B / H).
Lemma norm_quotient_pre A C :
-
A \subset 'N(H) → A / H \subset 'N(C) → A \subset 'N(coset H @*^-1 C).
+
A \subset 'N(H) → A / H \subset 'N(C) → A \subset 'N(coset H @*^-1 C).
-
Lemma cosetpre_normal C D :
(coset H @*^-1 C <| coset H @*^-1 D) = (C <| D).
+
Lemma cosetpre_normal C D :
(coset H @*^-1 C <| coset H @*^-1 D) = (C <| D).
-
Lemma quotient_normG G :
H <| G → 'N(G) / H = 'N(G / H).
+
Lemma quotient_normG G :
H <| G → 'N(G) / H = 'N(G / H).
-
Lemma quotient_subnormG A G :
H <| G → 'N_A(G) / H = 'N_(A / H)(G / H).
+
Lemma quotient_subnormG A G :
H <| G → 'N_A(G) / H = 'N_(A / H)(G / H).
-
Lemma cosetpre_cent1 x :
'C_('N(H))[x] \subset coset H @*^-1 'C[coset H x].
+
Lemma cosetpre_cent1 x :
'C_('N(H))[x] \subset coset H @*^-1 'C[coset H x].
Lemma cosetpre_cent1s C x :
-
coset H @*^-1 C \subset 'C[x] → C \subset 'C[coset H x].
+
coset H @*^-1 C \subset 'C[x] → C \subset 'C[coset H x].
Lemma cosetpre_subcent1 C x :
-
'C_(coset H @*^-1 C)[x] \subset coset H @*^-1 'C_C[coset H x].
+
'C_(coset H @*^-1 C)[x] \subset coset H @*^-1 'C_C[coset H x].
-
Lemma cosetpre_cent A :
'C_('N(H))(A) \subset coset H @*^-1 'C(A / H).
+
Lemma cosetpre_cent A :
'C_('N(H))(A) \subset coset H @*^-1 'C(A / H).
-
Lemma cosetpre_cents A C :
coset H @*^-1 C \subset 'C(A) → C \subset 'C(A / H).
+
Lemma cosetpre_cents A C :
coset H @*^-1 C \subset 'C(A) → C \subset 'C(A / H).
Lemma cosetpre_subcent C A :
-
'C_(coset H @*^-1 C)(A) \subset coset H @*^-1 'C_C(A / H).
+
'C_(coset H @*^-1 C)(A) \subset coset H @*^-1 'C_C(A / H).
-
Lemma restrm_quotientE G A (
nHG :
G \subset 'N(H)) :
-
A \subset G → restrm nHG (
coset H)
@* A = A / H.
+
Lemma restrm_quotientE G A (
nHG :
G \subset 'N(H)) :
+
A \subset G → restrm nHG (
coset H)
@* A = A / H.
Section InverseImage.
-
Variables (
G :
{group gT}) (
Kbar :
{group coset_of H}).
+
Variables (
G :
{group gT}) (
Kbar :
{group coset_of H}).
-
Hypothesis nHG :
H <| G.
+
Hypothesis nHG :
H <| G.
-
CoInductive inv_quotient_spec (
P :
pred {group gT}) :
Prop :=
-
InvQuotientSpec K of Kbar :=: K / H &
H \subset K &
P K.
+
Variant inv_quotient_spec (
P :
pred {group gT}) :
Prop :=
+
InvQuotientSpec K of Kbar :=: K / H &
H \subset K &
P K.
Lemma inv_quotientS :
-
Kbar \subset G / H → inv_quotient_spec (
fun K ⇒
K \subset G).
+
Kbar \subset G / H → inv_quotient_spec (
fun K ⇒
K \subset G).
-
Lemma inv_quotientN :
Kbar <| G / H → inv_quotient_spec (
fun K ⇒
K <| G).
+
Lemma inv_quotientN :
Kbar <| G / H → inv_quotient_spec (
fun K ⇒
K <| G).
End InverseImage.
-
Lemma quotientMidr A :
A × H / H = A / H.
+
Lemma quotientMidr A :
A × H / H = A / H.
-
Lemma quotientMidl A :
H × A / H = A / H.
+
Lemma quotientMidl A :
H × A / H = A / H.
-
Lemma quotientYidr G :
G \subset 'N(H) → G <*> H / H = G / H.
+
Lemma quotientYidr G :
G \subset 'N(H) → G <*> H / H = G / H.
-
Lemma quotientYidl G :
G \subset 'N(H) → H <*> G / H = G / H.
+
Lemma quotientYidl G :
G \subset 'N(H) → H <*> G / H = G / H.
Section Injective.
-
Variables (
G :
{group gT}).
-
Hypotheses (
nHG :
G \subset 'N(H)) (
tiHG :
H :&: G = 1).
+
Variables (
G :
{group gT}).
+
Hypotheses (
nHG :
G \subset 'N(H)) (
tiHG :
H :&: G = 1).
-
Lemma quotient_isom :
isom G (
G / H) (
restrm nHG (
coset H)).
+
Lemma quotient_isom :
isom G (
G / H) (
restrm nHG (
coset H)).
-
Lemma quotient_isog :
isog G (
G / H).
+
Lemma quotient_isog :
isog G (
G / H).
End Injective.
@@ -642,22 +641,22 @@
End CosetOfGroupTheory.
-
Notation "A / H" := (
quotient_group A H) :
Group_scope.
+
Notation "A / H" := (
quotient_group A H) :
Group_scope.
Section Quotient1.
-
Variables (
gT :
finGroupType) (
A :
{set gT}).
+
Variables (
gT :
finGroupType) (
A :
{set gT}).
-
Lemma coset1_injm :
'injm (@
coset gT 1
).
+
Lemma coset1_injm :
'injm (@
coset gT 1
).
-
Lemma quotient1_isom :
isom A (
A / 1) (
coset 1).
+
Lemma quotient1_isom :
isom A (
A / 1) (
coset 1).
-
Lemma quotient1_isog :
isog A (
A / 1).
+
Lemma quotient1_isog :
isog A (
A / 1).
End Quotient1.
@@ -666,48 +665,48 @@
Section QuotientMorphism.
-
Variable (
gT rT :
finGroupType) (
G H :
{group gT}) (
f :
{morphism G >-> rT}).
+
Variable (
gT rT :
finGroupType) (
G H :
{group gT}) (
f :
{morphism G >-> rT}).
-
Implicit Types A :
{set gT}.
-
Implicit Types B :
{set (coset_of H)}.
-
Hypotheses (
nsHG :
H <| G).
-
Let sHG :
H \subset G :=
normal_sub nsHG.
-
Let nHG :
G \subset 'N(H) :=
normal_norm nsHG.
-
Let nfHfG :
f @* G \subset 'N(f @* H) :=
morphim_norms f nHG.
+
Implicit Types A :
{set gT}.
+
Implicit Types B :
{set (coset_of H)}.
+
Hypotheses (
nsHG :
H <| G).
+
Let sHG :
H \subset G :=
normal_sub nsHG.
+
Let nHG :
G \subset 'N(H) :=
normal_norm nsHG.
+
Let nfHfG :
f @* G \subset 'N(f @* H) :=
morphim_norms f nHG.
-
Notation fH := (
coset (
f @* H)
\o f).
+
Notation fH := (
coset (
f @* H)
\o f).
-
Lemma quotm_dom_proof :
G \subset 'dom fH.
+
Lemma quotm_dom_proof :
G \subset 'dom fH.
Notation fH_G := (
restrm quotm_dom_proof fH).
-
Lemma quotm_ker_proof :
'ker (coset H) \subset 'ker fH_G.
+
Lemma quotm_ker_proof :
'ker (coset H) \subset 'ker fH_G.
Definition quotm :=
factm quotm_ker_proof nHG.
-
Canonical quotm_morphism :=
[morphism G / H of quotm].
+
Canonical quotm_morphism :=
[morphism G / H of quotm].
-
Lemma quotmE x :
x \in G → quotm (
coset H x)
= coset (
f @* H) (
f x).
+
Lemma quotmE x :
x \in G → quotm (
coset H x)
= coset (
f @* H) (
f x).
-
Lemma morphim_quotm A :
quotm @* (A / H) = f @* A / f @* H.
+
Lemma morphim_quotm A :
quotm @* (A / H) = f @* A / f @* H.
-
Lemma morphpre_quotm Abar :
quotm @*^-1 (Abar / f @* H) = f @*^-1 Abar / H.
+
Lemma morphpre_quotm Abar :
quotm @*^-1 (Abar / f @* H) = f @*^-1 Abar / H.
-
Lemma ker_quotm :
'ker quotm = 'ker f / H.
+
Lemma ker_quotm :
'ker quotm = 'ker f / H.
-
Lemma injm_quotm :
'injm f → 'injm quotm.
+
Lemma injm_quotm :
'injm f → 'injm quotm.
End QuotientMorphism.
@@ -716,52 +715,52 @@
Section EqIso.
-
Variables (
gT :
finGroupType) (
G H :
{group gT}).
+
Variables (
gT :
finGroupType) (
G H :
{group gT}).
-
Hypothesis (
eqGH :
G :=: H).
+
Hypothesis (
eqGH :
G :=: H).
-
Lemma im_qisom_proof :
'N(H) \subset 'N(G).
-
Lemma qisom_ker_proof :
'ker (coset G) \subset 'ker (coset H).
-
Lemma qisom_restr_proof :
setT \subset 'N(H) / G.
+
Lemma im_qisom_proof :
'N(H) \subset 'N(G).
+
Lemma qisom_ker_proof :
'ker (coset G) \subset 'ker (coset H).
+
Lemma qisom_restr_proof :
setT \subset 'N(H) / G.
Definition qisom :=
restrm qisom_restr_proof (
factm qisom_ker_proof im_qisom_proof).
-
Canonical qisom_morphism :=
Eval hnf in [morphism of qisom].
+
Canonical qisom_morphism :=
Eval hnf in [morphism of qisom].
-
Lemma qisomE x :
qisom (
coset G x)
= coset H x.
+
Lemma qisomE x :
qisom (
coset G x)
= coset H x.
-
Lemma val_qisom Gx :
val (
qisom Gx)
= val Gx.
+
Lemma val_qisom Gx :
val (
qisom Gx)
= val Gx.
-
Lemma morphim_qisom A :
qisom @* (A / G) = A / H.
+
Lemma morphim_qisom A :
qisom @* (A / G) = A / H.
-
Lemma morphpre_qisom A :
qisom @*^-1 (A / H) = A / G.
+
Lemma morphpre_qisom A :
qisom @*^-1 (A / H) = A / G.
-
Lemma injm_qisom :
'injm qisom.
+
Lemma injm_qisom :
'injm qisom.
-
Lemma im_qisom :
qisom @* setT = setT.
+
Lemma im_qisom :
qisom @* setT = setT.
Lemma qisom_isom :
isom setT setT qisom.
-
Lemma qisom_isog :
[set: coset_of G] \isog [set: coset_of H].
+
Lemma qisom_isog :
[set: coset_of G] \isog [set: coset_of H].
-
Lemma qisom_inj :
injective qisom.
+
Lemma qisom_inj :
injective qisom.
-
Lemma morphim_qisom_inj :
injective (
fun Gx ⇒
qisom @* Gx).
+
Lemma morphim_qisom_inj :
injective (
fun Gx ⇒
qisom @* Gx).
End EqIso.
@@ -775,23 +774,23 @@
Variables aT rT :
finGroupType.
-
Lemma first_isom (
G :
{group aT}) (
f :
{morphism G >-> rT}) :
-
{g : {morphism G / 'ker f >-> rT} | 'injm g &
-
∀ A :
{set aT},
g @* (A / 'ker f) = f @* A}.
+
Lemma first_isom (
G :
{group aT}) (
f :
{morphism G >-> rT}) :
+
{g : {morphism G / 'ker f >-> rT} | 'injm g &
+
∀ A :
{set aT},
g @* (A / 'ker f) = f @* A}.
-
Variables (
G H :
{group aT}) (
f :
{morphism G >-> rT}).
-
Hypothesis sHG :
H \subset G.
+
Variables (
G H :
{group aT}) (
f :
{morphism G >-> rT}).
+
Hypothesis sHG :
H \subset G.
-
Lemma first_isog :
(G / 'ker f) \isog (f @* G).
+
Lemma first_isog :
(G / 'ker f) \isog (f @* G).
-
Lemma first_isom_loc :
{g : {morphism H / 'ker_H f >-> rT} |
-
'injm g & ∀ A :
{set aT},
A \subset H → g @* (A / 'ker_H f) = f @* A}.
+
Lemma first_isom_loc :
{g : {morphism H / 'ker_H f >-> rT} |
+
'injm g & ∀ A :
{set aT},
A \subset H → g @* (A / 'ker_H f) = f @* A}.
-
Lemma first_isog_loc :
(H / 'ker_H f) \isog (f @* H).
+
Lemma first_isog_loc :
(H / 'ker_H f) \isog (f @* H).
End FirstIsomorphism.
@@ -800,20 +799,20 @@
Section SecondIsomorphism.
-
Variables (
gT :
finGroupType) (
H K :
{group gT}).
+
Variables (
gT :
finGroupType) (
H K :
{group gT}).
-
Hypothesis nKH :
H \subset 'N(K).
+
Hypothesis nKH :
H \subset 'N(K).
-
Lemma second_isom :
{f : {morphism H / (K :&: H) >-> coset_of K} |
-
'injm f & ∀ A :
{set gT},
A \subset H → f @* (A / (K :&: H)) = A / K}.
+
Lemma second_isom :
{f : {morphism H / (K :&: H) >-> coset_of K} |
+
'injm f & ∀ A :
{set gT},
A \subset H → f @* (A / (K :&: H)) = A / K}.
-
Lemma second_isog :
H / (K :&: H) \isog H / K.
+
Lemma second_isog :
H / (K :&: H) \isog H / K.
-
Lemma weak_second_isog :
H / (K :&: H) \isog H × K / K.
+
Lemma weak_second_isog :
H / (K :&: H) \isog H × K / K.
End SecondIsomorphism.
@@ -822,30 +821,30 @@
Section ThirdIsomorphism.
-
Variables (
gT :
finGroupType) (
G H K :
{group gT}).
+
Variables (
gT :
finGroupType) (
G H K :
{group gT}).
-
Lemma homg_quotientS (
A :
{set gT}) :
-
A \subset 'N(H) → A \subset 'N(K) → H \subset K → A / K \homg A / H.
+
Lemma homg_quotientS (
A :
{set gT}) :
+
A \subset 'N(H) → A \subset 'N(K) → H \subset K → A / K \homg A / H.
-
Hypothesis sHK :
H \subset K.
-
Hypothesis snHG :
H <| G.
-
Hypothesis snKG :
K <| G.
+
Hypothesis sHK :
H \subset K.
+
Hypothesis snHG :
H <| G.
+
Hypothesis snKG :
K <| G.
-
Theorem third_isom :
{f : {morphism (G / H) / (K / H) >-> coset_of K} | 'injm f
-
& ∀ A :
{set gT},
A \subset G → f @* (A / H / (K / H)) = A / K}.
+
Theorem third_isom :
{f : {morphism (G / H) / (K / H) >-> coset_of K} | 'injm f
+
& ∀ A :
{set gT},
A \subset G → f @* (A / H / (K / H)) = A / K}.
-
Theorem third_isog :
(G / H / (K / H)) \isog (G / K).
+
Theorem third_isog :
(G / H / (K / H)) \isog (G / K).
End ThirdIsomorphism.
-
Lemma char_from_quotient (
gT :
finGroupType) (
G H K :
{group gT}) :
-
H <| K → H \char G → K / H \char G / H → K \char G.
+
Lemma char_from_quotient (
gT :
finGroupType) (
G H K :
{group gT}) :
+
H <| K → H \char G → K / H \char G / H → K \char G.
-Variables (aT rT : finGroupType) (D : {group aT}) (f : {morphism D >-> rT}).
-Implicit Types G H : {group aT}.
-Implicit Types L M : {group rT}.
+Variables (aT rT : finGroupType) (D : {group aT}) (f : {morphism D >-> rT}).
+Implicit Types G H : {group aT}.
+Implicit Types L M : {group rT}.
-Lemma card_morphim G : #|f @* G| = #|D :&: G : 'ker f|.
+Lemma card_morphim G : #|f @* G| = #|D :&: G : 'ker f|.
-Lemma dvdn_morphim G : #|f @* G| %| #|G|.
+Lemma dvdn_morphim G : #|f @* G| %| #|G|.
-Lemma logn_morphim p G : logn p #|f @* G| ≤ logn p #|G|.
+Lemma logn_morphim p G : logn p #|f @* G| ≤ logn p #|G|.
-Lemma coprime_morphl G p : coprime #|G| p → coprime #|f @* G| p.
+Lemma coprime_morphl G p : coprime #|G| p → coprime #|f @* G| p.
-Lemma coprime_morphr G p : coprime p #|G| → coprime p #|f @* G|.
+Lemma coprime_morphr G p : coprime p #|G| → coprime p #|f @* G|.
-Lemma coprime_morph G H : coprime #|G| #|H| → coprime #|f @* G| #|f @* H|.
+Lemma coprime_morph G H : coprime #|G| #|H| → coprime #|f @* G| #|f @* H|.
Lemma index_morphim_ker G H :
- H \subset G → G \subset D →
- (#|f @* G : f @* H| × #|'ker_G f : H|)%N = #|G : H|.
+ H \subset G → G \subset D →
+ (#|f @* G : f @* H| × #|'ker_G f : H|)%N = #|G : H|.
-Lemma index_morphim G H : G :&: H \subset D → #|f @* G : f @* H| %| #|G : H|.
+Lemma index_morphim G H : G :&: H \subset D → #|f @* G : f @* H| %| #|G : H|.
-Lemma index_injm G H : 'injm f → G \subset D → #|f @* G : f @* H| = #|G : H|.
+Lemma index_injm G H : 'injm f → G \subset D → #|f @* G : f @* H| = #|G : H|.
-Lemma card_morphpre L : L \subset f @* D → #|f @*^-1 L| = (#|'ker f| × #|L|)%N.
+Lemma card_morphpre L : L \subset f @* D → #|f @*^-1 L| = (#|'ker f| × #|L|)%N.
Lemma index_morphpre L M :
- L \subset f @* D → #|f @*^-1 L : f @*^-1 M| = #|L : M|.
+ L \subset f @* D → #|f @*^-1 L : f @*^-1 M| = #|L : M|.
End CardMorphism.
-Lemma card_homg (aT rT : finGroupType) (G : {group aT}) (R : {group rT}) :
- G \homg R → #|G| %| #|R|.
+Lemma card_homg (aT rT : finGroupType) (G : {group aT}) (R : {group rT}) :
+ G \homg R → #|G| %| #|R|.
Section CardCosetpre.
-Variables (gT : finGroupType) (G H K : {group gT}) (L M : {group coset_of H}).
+Variables (gT : finGroupType) (G H K : {group gT}) (L M : {group coset_of H}).
-Lemma dvdn_quotient : #|G / H| %| #|G|.
+Lemma dvdn_quotient : #|G / H| %| #|G|.
Lemma index_quotient_ker :
- K \subset G → G \subset 'N(H) →
- (#|G / H : K / H| × #|G :&: H : K|)%N = #|G : K|.
+ K \subset G → G \subset 'N(H) →
+ (#|G / H : K / H| × #|G :&: H : K|)%N = #|G : K|.
-Lemma index_quotient : G :&: K \subset 'N(H) → #|G / H : K / H| %| #|G : K|.
+Lemma index_quotient : G :&: K \subset 'N(H) → #|G / H : K / H| %| #|G : K|.
Lemma index_quotient_eq :
- G :&: H \subset K → K \subset G → G \subset 'N(H) →
- #|G / H : K / H| = #|G : K|.
+ G :&: H \subset K → K \subset G → G \subset 'N(H) →
+ #|G / H : K / H| = #|G : K|.
-Lemma card_cosetpre : #|coset H @*^-1 L| = (#|H| × #|L|)%N.
+Lemma card_cosetpre : #|coset H @*^-1 L| = (#|H| × #|L|)%N.
-Lemma index_cosetpre : #|coset H @*^-1 L : coset H @*^-1 M| = #|L : M|.
+Lemma index_cosetpre : #|coset H @*^-1 L : coset H @*^-1 M| = #|L : M|.
End CardCosetpre.
--
cgit v1.2.3