A group with a finitely generated subgroup of finite index is finitely generated

Proved

GroupFiniteness.fg_of_fg_of_finiteIndex

by dbenbenn · Sep 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatorial-group-theoryfinitely-presented-groupsgroup-theory

Let $H$ be a subgroup of finite index in a group $G$ , and suppose that $H$ is finitely generated. Then $G$ is finitely generated.

Nothing is asserted about the number of generators: the conclusion is the bare existence of a finite generating set. One can be obtained by taking a finite generating set of $H$ together with one representative of each of the finitely many cosets of $H$ , since every $g \in G$ is the representative of its own coset times an element of $H$ . The subgroup is not assumed normal.

Preamble

import Mathlib

Formal statement

namespace GroupFiniteness

theorem fg_of_fg_of_finiteIndex {G : Type*} [Group G] (H : Subgroup G)
    [H.FiniteIndex] [Group.FG H] : Group.FG G := by
  sorry

end GroupFiniteness

Source

The converse of Schreier's lemma. Mathlib has Schreier's lemma itself, `Subgroup.fg_of_index_ne_zero`: a subgroup of finite index in a finitely generated group is finitely generated. It does not have this direction, which is needed wherever a property is transferred from a finite-index subgroup to the whole group, as in Wolf's Proposition 4.1.

View graph