Theorems · Theorem · group theory

AddSubgroup.closure_add_image_eq_top

∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {R S : Set G} (hR : AddSubgroup.IsComplement (↑H) R),
  0 ∈ R → AddSubgroup.closure S = ⊤ → AddSubgroup.closure ((fun g => ⟨g + -↑(hR.toRightFun g), ⋯⟩) '' (R + S)) = ⊤

Schreier's Lemma: If R : Set G and H : AddSubgroup G are complements with 0 ∈ R, and if G is generated by S : Set G, then H is generated by the Set (R + S).image (fun g ↦ g - (hR.toRightFun g)).

Defined in

Mathlib.GroupTheory.Schreier

Cited by

1 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddGroup