# Schreier's Lemma #

In this file we prove Schreier's lemma.

## Main results #

• closure_mul_image_eq : Schreier's Lemma: If R : Set G is a right_transversal 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)⁻¹).
• 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.
theorem card_dvd_exponent_nsmul_rank (G : Type u_1) [] [] :
theorem card_dvd_exponent_pow_rank (G : Type u_1) [] [] :
theorem card_dvd_exponent_nsmul_rank' (G : Type u_1) [] [] {n : } (hG : ∀ (g : G), n g = 0) :
theorem card_dvd_exponent_pow_rank' (G : Type u_1) [] [] {n : } (hG : ∀ (g : G), g ^ n = 1) :
n ^
theorem Subgroup.closure_mul_image_mul_eq_top {G : Type u_1} [] {H : } {R : Set G} {S : Set G} (hR : ) (hR1 : 1 R) (hS : ) :
(Subgroup.closure ((fun (g : G) => g * (↑)⁻¹) '' (R * S))) * R =
theorem Subgroup.closure_mul_image_eq {G : Type u_1} [] {H : } {R : Set G} {S : Set G} (hR : ) (hR1 : 1 R) (hS : ) :
Subgroup.closure ((fun (g : G) => g * (↑)⁻¹) '' (R * S)) = H

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)⁻¹).

theorem Subgroup.closure_mul_image_eq_top {G : Type u_1} [] {H : } {R : Set G} {S : Set G} (hR : ) (hR1 : 1 R) (hS : ) :
Subgroup.closure ((fun (g : G) => g * (↑)⁻¹, ) '' (R * S)) =

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)⁻¹).

theorem Subgroup.closure_mul_image_eq_top' {G : Type u_1} [] {H : } [] {R : } {S : } (hR : ) (hR1 : 1 R) (hS : ) :
Subgroup.closure (Finset.image (fun (g : G) => g * (↑)⁻¹, ) (R * S)) =

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)⁻¹).

theorem Subgroup.exists_finset_card_le_mul {G : Type u_1} [] (H : ) [H.FiniteIndex] {S : } (hS : ) :
∃ (T : Finset { x : G // x H }), T.card H.index * S.card
instance Subgroup.fg_of_index_ne_zero {G : Type u_1} [] (H : ) [hG : ] [H.FiniteIndex] :
Group.FG { x : G // x H }

Schreier's Lemma: A finite index subgroup of a finitely generated group is finitely generated.

Equations
• =
theorem Subgroup.rank_le_index_mul_rank {G : Type u_1} [] (H : ) [hG : ] [H.FiniteIndex] :
Group.rank { x : G // x H } H.index *
theorem Subgroup.card_commutator_dvd_index_center_pow (G : Type u_1) [] [Finite ] :
Nat.card { x : G // x } .index ^ (.index * + 1)

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 bound for the size of the commutator subgroup in terms of the number of commutators.

Equations
• = (n ^ (2 * n)) ^ (n ^ (2 * n + 1) + 1)
Instances For

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
• =