p-adic Valuation

This file defines the p-adic valuation on ℕ, ℤ, and ℚ.

The p-adic valuation on ℚ is the difference of the multiplicities of p in the numerator and denominator of q. This function obeys the standard properties of a valuation, with the appropriate assumptions on p. The p-adic valuations on ℕ and ℤ agree with that on ℚ.

The valuation induces a norm on ℚ. This norm is defined in Mathlib/NumberTheory/Padics/PadicNorm.lean.

theorem padicValNat_eq_emultiplicity_of_ne_one {p : ℕ} (hp : p ≠ 1) {n : ℕ} (hn : n ≠ 0) : ↑(padicValNat p n) = emultiplicity p n

@[simp]

theorem Nat.toNat_emultiplicity (p n : ℕ) : (emultiplicity p n).toNat = padicValNat p n

@[deprecated Nat.padicValNat_def (since := "2026-09-08")]

theorem padicValNat_def' {p n : ℕ} : padicValNat p n = multiplicity p n

Alias of Nat.padicValNat_def.

theorem padicValNat_eq_emultiplicity {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : n ≠ 0) : ↑(padicValNat p n) = emultiplicity p n

A simplification of padicValNat when one input is prime, by analogy with padicValRat_def.

@[deprecated padicValNat_eq_emultiplicity (since := "2026-03-15")]

theorem padicValNat.maxPowDiv_eq_emultiplicity {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : n ≠ 0) : ↑(padicValNat p n) = emultiplicity p n

Alias of padicValNat_eq_emultiplicity.

---

A simplification of padicValNat when one input is prime, by analogy with padicValRat_def.

@[deprecated Nat.padicValNat_def (since := "2026-03-15")]

theorem padicValNat.maxPowDiv_eq_multiplicity {p n : ℕ} : padicValNat p n = multiplicity p n

Alias of Nat.padicValNat_def.

@[deprecated padicValNat_zero_right (since := "2026-03-15")]

theorem padicValNat.zero {p : ℕ} : padicValNat p 0 = 0

@[deprecated padicValNat_one_right (since := "2026-03-15")]

theorem padicValNat.one {p : ℕ} : padicValNat p 1 = 0

@[simp]

theorem padicValNat.eq_zero_iff {p n : ℕ} : padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n

theorem le_emultiplicity_iff_replicate_subperm_primeFactorsList {a b n : ℕ} (ha : Nat.Prime a) (hb : b ≠ 0) : ↑n ≤ emultiplicity a b ↔ (List.replicate n a).Subperm b.primeFactorsList

theorem le_padicValNat_iff_replicate_subperm_primeFactorsList {a b n : ℕ} (ha : Nat.Prime a) (hb : b ≠ 0) : n ≤ padicValNat a b ↔ (List.replicate n a).Subperm b.primeFactorsList

theorem mul_padicValNat_le {p n : ℕ} : p * padicValNat p n ≤ n

A weak upper bound on padicValNat p n.