Positive powers of fundamental units still generate a subgroup of finite index

Proved

Leopoldt.finiteIndex_closure_pow_fundSystem

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

number-theoryunits

Let $K$ be a number field and $u_1,\dots,u_r$ a fundamental system of global units. For every positive integer $m$ , the subgroup generated by $u_1^m,\dots,u_r^m$ has finite index in $\mathcal O_K^\times$ :

[\mathcal O_K^\times:\langle u_1^m,\dots,u_r^m\rangle]<\infty.

This lets one replace fundamental units by powers chosen to enter a small $p$ -adic logarithm ball, while retaining the finite-index hypothesis needed by the logarithmic criterion.

Preamble

import Definitions.Def_PadicLog

open NumberField

Formal statement

namespace Leopoldt
theorem finiteIndex_closure_pow_fundSystem
    (K : Type*) [Field K] [NumberField K] (m : ℕ) (hm : 0 < m) :
    (Subgroup.closure (Set.range fun i => NumberField.Units.fundSystem K i ^ m)).FiniteIndex := by sorry
end Leopoldt

Source

Extraction of a finite-index unit-power lemma from the verified proof of Leopoldt.leopoldtConjecture_iff_exists_linearIndependent_log_conj (submission 48251889-2ea0-4f5b-804c-e937ba97f5d3); Dirichlet unit theorem and finite generation of number-field units.

View graph