# mathlib3documentation

group_theory.schreier

# Schreier's Lemma #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.
• card_commutator_le_of_finite_commutator_set: 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} [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) [H.finite_index] {S : finset G} (hS : = ) :
(T : finset H), T.card H.index * S.card
@[protected, instance]
def subgroup.fg_of_index_ne_zero {G : Type u_1} [group G] (H : subgroup G) [hG : group.fg G] [H.finite_index] :

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

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)

A theorem of Schur: The size of the commutator subgroup is bounded in terms of the number of commutators.

@[protected, instance]

A theorem of Schur: A group with finitely many commutators has finite commutator subgroup.