fg_of_index_ne_zero — Mathlib

English

A subgroup H of a finitely generated group G with finite index is itself finitely generated.

Русский

Подгруппа H конечного индекса в конечной генераторной группе G тоже конечносгенерируемая.

LaTeX

$$If [H] is finite index in G and G is finitely generated, then H is finitely generated.$$

Lean4

/-- **Schreier's Lemma**: A finite index subgroup of a finitely generated
  group is finitely generated. -/
instance fg_of_index_ne_zero [hG : Group.FG G] [FiniteIndex H] : Group.FG H :=
  by
  obtain ⟨S, hS⟩ := hG.1
  obtain ⟨T, -, hT⟩ := exists_finset_card_le_mul H hS
  exact ⟨⟨T, hT⟩⟩

Похожие утверждения