mathlib documentation

group_theory.schreier

Schreier's Lemma #

In this file we prove Schreier's lemma.

Main results #

theorem subgroup.closure_mul_image_mul_eq_top {G : Type u_1} [group G] {H : subgroup G} {R S : set G} (hR : R subgroup.right_transversals H) (hR1 : 1 R) (hS : subgroup.closure S = ) :
theorem subgroup.closure_mul_image_eq {G : Type u_1} [group G] {H : subgroup G} {R S : set G} (hR : R subgroup.right_transversals H) (hR1 : 1 R) (hS : subgroup.closure 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} {R S : set G} (hR : R subgroup.right_transversals H) (hR1 : 1 R) (hS : subgroup.closure 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 subgroup.right_transversals H) (hR1 : 1 R) (hS : subgroup.closure 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 : subgroup.closure S = ) :
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) [decidable_pred (λ (n : ), ∃ (S : finset G), S.card = n subgroup.closure S = )] [decidable_pred (λ (n : ), ∃ (S : finset H), S.card = n subgroup.closure S = )] :