# Documentation

Mathlib.GroupTheory.Schreier

# 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 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 * ()⁻¹) '' (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 * ()⁻¹) '' (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 => { val := g * ()⁻¹, property := (_ : g * ()⁻¹ H) }) '' (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 => { val := g * ()⁻¹, property := (_ : g * ()⁻¹ H) }) (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 : ) {S : } (hS : ) :
T,
instance Subgroup.fg_of_index_ne_zero {G : Type u_1} [] (H : ) [hG : ] :
Group.FG { x // x H }

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

theorem Subgroup.rank_le_index_mul_rank {G : Type u_1} [] (H : ) [hG : ] :
Group.rank { x // x H }
theorem Subgroup.card_commutator_dvd_index_center_pow (G : Type u_1) [] [Finite ↑()] :
Nat.card { x // x } ^ ( + 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.

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.