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 multiplicity_eq_emultiplicity_of_ne_one {p : ℕ} (hp : p ≠ 1) {n : ℕ} (hn : n ≠ 0) : ↑(multiplicity p n) = emultiplicity p n

@[deprecated multiplicity_eq_emultiplicity_of_ne_one (since := "2026-10-28")]

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

Alias of multiplicity_eq_emultiplicity_of_ne_one.

@[simp]

theorem Nat.toNat_emultiplicity (p n : ℕ) : (emultiplicity p n).toNat = multiplicity 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 multiplicity_eq_emultiplicity {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : n ≠ 0) : ↑(multiplicity p n) = emultiplicity p n

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

@[deprecated multiplicity_eq_emultiplicity (since := "2026-10-28")]

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

Alias of multiplicity_eq_emultiplicity.

---

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

@[simp]

theorem Nat.multiplicity_eq_zero_iff {p n : ℕ} : multiplicity p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n

@[deprecated Nat.multiplicity_eq_zero_iff (since := "2026-10-28")]

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

Alias of Nat.multiplicity_eq_zero_iff.

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_multiplicity_iff_replicate_subperm_primeFactorsList {a b n : ℕ} (ha : Nat.Prime a) (hb : b ≠ 0) : n ≤ multiplicity a b ↔ (List.replicate n a).Subperm b.primeFactorsList

@[deprecated le_multiplicity_iff_replicate_subperm_primeFactorsList (since := "2026-10-28")]

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

Alias of le_multiplicity_iff_replicate_subperm_primeFactorsList.

theorem mul_multiplicity_le {p n : ℕ} : p * multiplicity p n ≤ n

A weak upper bound on multiplicity p n.

@[deprecated mul_multiplicity_le (since := "2026-10-28")]

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

Alias of mul_multiplicity_le.

---

A weak upper bound on multiplicity p n.