Padic unit squares form an open subgroup

Port of upstream Padics/Squares.lean. The squares among the p-adic units form an open subgroup of ℚ_[p]ˣ: every element close enough to 1 is a square, so the square locus is a neighbourhood of 1, and translation by an already-known square exhibits it as a neighbourhood of every one of its points.

The two lifting lemmas (PadicInt.isSquare_of_zmod, PadicInt.isSquare_of_zmodPow) are Hensel-style: a p-adic integer unit is a square as soon as its reduction modulo p (odd p) resp. modulo 8 (p = 2) is one. They are ported here because the upstream Padics/Squares.lean obtains them from Padics/Lemmas.lean.

Provenance

This file is a derived work. It is based on Padics/Squares.lean and Padics/Lemmas.lean of the HassePrinciple project (https://github.com/mariainesdff/HassePrinciple, Apache-2.0, Copyright (c) 2026 Nirvana Coppola, María Inés de Frutos-Fernández), a Women in Numbers 7 collaboration. It has been modified: the statements and proofs were rewritten for Lean 4.33 / Mathlib without upstream's module system, and the development is extended beyond what upstream proves. Upstream declaration names are kept so that the two developments can be compared side by side. See the repository NOTICE file.

Reduction criteria for p-adic integer squares

theorem PadicInt.p_dvd_iff_toZMod_eq_zero {p : ℕ} [Fact (Nat.Prime p)] {m : ℤ_[p]} : ↑p ∣ m ↔ toZMod m = 0

theorem PadicInt.pow_p_dvd_iff_toZModPow_eq_zero {p : ℕ} [Fact (Nat.Prime p)] {m : ℤ_[p]} {n : ℕ} : ↑p ^ n ∣ m ↔ (toZModPow n) m = 0

theorem PadicInt.isSquare_of_zmod {p : ℕ} [Fact (Nat.Prime p)] (hp : p ≠ 2) {m : ℤ_[p]} (hm : ¬↑p ∣ m) (hmod : IsSquare (toZMod m)) : IsSquare m

theorem PadicInt.isSquare_of_zmodPow {m : ℤ_[2]} (hm : ¬2 ∣ m) (hmod : IsSquare ((toZModPow 3) m)) : IsSquare m

Near 1 the p-adic units are squares

theorem Padic.isSquare_of_dist_one_lt_one {p : ℕ} [Fact (Nat.Prime p)] (hp : p ≠ 2) {x : ℚ_[p]} (hx : dist x 1 < 1) : IsSquare x

theorem Padic.isSquare_of_dist_one_lt_pow {x : ℚ_[2]} (hx : dist x 1 < 2 ^ (-2)) : IsSquare x

theorem Padic.exists_pow_isSquare_of_dist_one_lt (p : ℕ) [Fact (Nat.Prime p)] : ∃ (n : ℕ), ∀ (x : ℚ_[p]), dist x 1 < ↑p ^ (-↑n) → IsSquare x

theorem Padic.isOpen_squares_sdiff_zero (p : ℕ) [Fact (Nat.Prime p)] : IsOpen ({x : ℚ_[p] | IsSquare x} \ {0})

def Padic.unitSquares (p : ℕ) [Fact (Nat.Prime p)] : OpenSubgroup ℚ_[p]ˣ

The open subgroup of p-adic unit squares inside ℚ_[p]ˣ.

Equations

• Padic.unitSquares p = { carrier := {x : ℚ_[p]ˣ | IsSquare x}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯, isOpen' := ⋯ }