Prove2Me

Bounded pp-adic rank is unchanged under power-saturated subgroup inclusion

Proved
Leopoldt.zpRankBelow_eq_of_power_mem

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

number-theoryp-adicunits

Let H′⊆HH'\subseteq H be subgroups of a commutative topological group, and suppose there is a nonzero integer mm such that every mmth power of an element of HH belongs to H′H'. Then, for any fixed bound bb, their bounded pp-adic ranks agree:

rank⁡p,≤b(H′)=rank⁡p,≤b(H).\operatorname{rank}_{p,\le b}(H')=\operatorname{rank}_{p,\le b}(H).

In particular, the power condition is the key step in showing that passage to a subgroup of finite index preserves the free pp-adic rank. The statement applies to the rank notion used for the closures of global units in the mission.

Formalization Note The source rank witnesses are continuous injections of Zpn\mathbb Z_p^n; multiplication by a nonzero integer on this source remains continuous and injective.

Preamble
import Definitions.Def_LeopoldtDefect
Formal statement
namespace Leopoldt
theorem zpRankBelow_eq_of_power_mem (p : ℕ) [Fact p.Prime]
    {G : Type*} [CommGroup G] [TopologicalSpace G]
    (b : ℕ) {H H' : Subgroup G} (hsub : H' ≤ H)
    (m : ℕ) (hm : m ≠ 0) (hpow : ∀ x ∈ H, x ^ m ∈ H') :
    zpRankBelow p b H' = zpRankBelow p b H := by sorry
end Leopoldt
Source
Formal consequence of the bounded p-adic rank definition in Definitions.Def_LeopoldtDefect, which formalizes Preda Mihăilescu, On CM Z_p-extensions and the Leopoldt conjecture for CM fields, arXiv:1105.4544v4, Section 1.1, p. 3 (p-adic rank of the closure of units). The power condition expresses the standard finite-index subgroup mechanism; compare Section 1.3, Remark 1.A, p. 5.

View graph