Powers preserve the finite-index span of a finite family in a commutative group

Proved

Leopoldt.finiteIndex_closure_range_pow

by xuanji · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebranumber-theoryunits

Let a finite family $(g_i)$ in a commutative group $G$ generate a subgroup of finite index. For every positive integer $n$ , the powers $(g_i^n)$ also generate a finite-index subgroup. Indeed, the first subgroup is finitely generated, and multiplication by $n$ has finite-index image in every finitely generated abelian group. This lemma preserves the finite-index condition of a Minkowski unit when it is raised to a power to enter a small $p$ -adic logarithm ball.

Preamble

import Mathlib.GroupTheory.FiniteAbelian.Basic
import Mathlib.GroupTheory.Finiteness

Formal statement

namespace Leopoldt
theorem finiteIndex_closure_range_pow (G : Type*) [CommGroup G]
    (ι : Type*) [Finite ι] (f : ι → G)
    (h : (Subgroup.closure (Set.range f)).FiniteIndex)
    (n : ℕ) (hn : n ≠ 0) :
    (Subgroup.closure (Set.range fun i => f i ^ n)).FiniteIndex := by sorry
end Leopoldt

Source

Elementary consequence of the structure theorem for finitely generated abelian groups, formalized in Mathlib as Subgroup.isFiniteRelIndex_map_powMonoidHom_of_fg. Applied to the Galois conjugates of a Minkowski unit in the Leopoldt mission (Preda Mihăilescu, On CM Z_p-extensions and the Leopoldt conjecture for CM fields, https://arxiv.org/abs/1105.4544, Section 1.1).

View graph