# mathlibdocumentation

group_theory.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 (λ g, g * (to_fun hR g)⁻¹).
• fg_of_index_ne_zero : Schreier's Lemma: A finite index subgroup of a finitely generated group is finitely generated.
theorem subgroup.closure_mul_image_mul_eq_top {G : Type u_1} [group G] {H : subgroup G} {R S : set G} (hR : R ) (hR1 : 1 R) (hS : = ) :
(subgroup.closure ((λ (g : G), g * '' (R * S))) * R =
theorem subgroup.closure_mul_image_eq {G : Type u_1} [group G] {H : subgroup G} {R S : set G} (hR : R ) (hR1 : 1 R) (hS : = ) :
subgroup.closure ((λ (g : G), g * '' (R * S)) = H

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 (λ g, g * (to_fun hR g)⁻¹).

theorem subgroup.closure_mul_image_eq_top {G : Type u_1} [group G] {H : subgroup G} {R S : set G} (hR : R ) (hR1 : 1 R) (hS : = ) :
subgroup.closure ((λ (g : G), , _⟩) '' (R * S)) =

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 (λ g, g * (to_fun hR g)⁻¹).

theorem subgroup.closure_mul_image_eq_top' {G : Type u_1} [group G] {H : subgroup G} [decidable_eq G] {R S : finset G} (hR : R ) (hR1 : 1 R) (hS : = ) :
subgroup.closure (finset.image (λ (g : G), , _⟩) (R * S)) =

Schreier's Lemma: If R : finset G is a right_transversal 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 (λ g, g * (to_fun hR g)⁻¹).

theorem subgroup.exists_finset_card_le_mul {G : Type u_1} [group G] {H : subgroup G} (hH : H.index 0) {S : finset G} (hS : = ) :
∃ (T : finset H), T.card H.index * S.card
theorem subgroup.fg_of_index_ne_zero {G : Type u_1} [group G] {H : subgroup G} [hG : group.fg G] (hH : H.index 0) :

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} [group G] [hG : group.fg G] {H : subgroup G} (hH : H.index 0) :
H.index *