An extension of a finitely generated group by a finitely generated group is finitely generated

Proved

GroupFiniteness.fg_of_extension

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

combinatorial-group-theoryfinitely-presented-groupsgroup-theory

Let $N$ be a normal subgroup of a group $G$ such that both $N$ and the quotient $G/N$ are finitely generated. Then $G$ is finitely generated: a finite generating set is given by a finite generating set of $N$ together with one preimage in $G$ of each element of a finite generating set of $G/N$ .

Preamble

import Mathlib

Formal statement

namespace GroupFiniteness

/-- An extension of a finitely generated group by a finitely generated group is finitely
generated: generators of `N` together with lifts of generators of `G ⧸ N` generate `G`. -/
theorem fg_of_extension {G : Type*} [Group G] (N : Subgroup G) [N.Normal]
    [Group.FG N] [Group.FG (G ⧸ N)] : Group.FG G := by
  sorry

end GroupFiniteness

Source

Standard elementary fact: generators of the normal subgroup together with lifts of generators of the quotient generate the group. Stated here because Mathlib has finite generation of subgroups of finite index (Schreier) and of quotients, but not of extensions.

View graph