Schreier's Lemma #
In this file we prove Schreier's lemma.
Main results #
closure_mul_image_eq
: Schreier's Lemma: IfR : Set G
is a right_transversal ofH : Subgroup G
with1 ∈ R
, and ifG
is generated byS : Set G
, thenH
is generated by theSet
(R * S).image (fun g ↦ g * (toFun hR g)⁻¹)
.fg_of_index_ne_zero
: Schreier's Lemma: A finite index subgroup of a finitely generated group is finitely generated.card_commutator_le_of_finite_commutatorSet
: A theorem of Schur: The size of the commutator subgroup is bounded in terms of the number of commutators.
Schreier's Lemma: If R : Set G
is a rightTransversal
of H : Subgroup G
with 1 ∈ R
, and if G
is generated by S : Set G
, then H
is generated by the Set
(R * S).image (fun g ↦ g * (toFun hR g)⁻¹)
.
Schreier's Lemma: If R : Set G
is a rightTransversal
of H : Subgroup G
with 1 ∈ R
, and if G
is generated by S : Set G
, then H
is generated by the Set
(R * S).image (fun g ↦ g * (toFun hR g)⁻¹)
.
Schreier's Lemma: If R : Finset G
is a rightTransversal
of H : Subgroup G
with 1 ∈ R
, and if G
is generated by S : Finset G
, then H
is generated by the Finset
(R * S).image (fun g ↦ g * (toFun hR g)⁻¹)
.
If G
has n
commutators [g₁, g₂]
, then |G'| ∣ [G : Z(G)] ^ ([G : Z(G)] * n + 1)
,
where G'
denotes the commutator of G
.
A theorem of Schur: The size of the commutator subgroup is bounded in terms of the number of commutators.
A theorem of Schur: A group with finitely many commutators has finite commutator subgroup.
Equations
- ⋯ = ⋯