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.

Notation

This file uses the local notation /. for Rat.mk.

Implementation notes

Much, but not all, of this file assumes that p is prime. This assumption is inferred automatically by taking [Fact p.Prime] as a type class argument.

Calculations with p-adic valuations

• multiplicity_factorial: Legendre's Theorem. The p-adic valuation of n! is the sum of the quotients n / p ^ i. This sum is expressed over the finset Ico 1 b where b is any bound greater than log p n.

• Nat.Prime.sub_one_mul_multiplicity_factorial: Legendre's Theorem. Taking (p - 1) times the p-adic valuation of n! equals n minus the sum of base p digits of n.

• multiplicity_choose: Kummer's Theorem. The p-adic valuation of n.choose k is the number of carries when k and n - k are added in base p. This sum is expressed over the finset Ico 1 b where b is any bound greater than log p n.

• sub_one_mul_multiplicity_choose_eq_sub_sum_digits: Kummer's Theorem. Taking (p - 1) times the p-adic valuation of the binomial n over k equals the sum of the digits of k plus the sum of the digits of n - k minus the sum of digits of n, all base p.

References

• [F. Q. Gouvêa, p-adic numbers][gouvea1997]
• [R. Y. Lewis, A formal proof of Hensel's lemma over the p-adic integers][lewis2019]
• https://en.wikipedia.org/wiki/P-adic_number

Tags

p-adic, p adic, padic, norm, valuation

theorem Nat.multiplicity_dvd_of_ne_zero {p n : ℕ} (h : multiplicity p n ≠ 0) : p ∣ n

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

theorem padicValNat.self {p : ℕ} (hp : 1 < p) : multiplicity p p = 1

Alias of Nat.multiplicity_self.

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

theorem padicValNat.eq_zero_of_not_dvd {α : Type u_1} [Monoid α] {a b : α} (h : ¬a ∣ b) : multiplicity a b = 0

Alias of multiplicity_eq_zero_of_not_dvd.

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

theorem padicValNat.dvd_of_ne_zero {p n : ℕ} (h : multiplicity p n ≠ 0) : p ∣ n

Alias of Nat.multiplicity_dvd_of_ne_zero.

noncomputable def padicValInt (p : ℕ) (z : ℤ) : ℕ

For p ≠ 1, the p-adic valuation of an integer z ≠ 0 is the largest natural number k such that p^k divides z. If x = 0 or p = 1, then padicValInt p q defaults to 0.

Equations

• padicValInt p z = multiplicity p z.natAbs

theorem padicValInt.of_ne_one_ne_zero {p : ℕ} {z : ℤ} : padicValInt p z = multiplicity (↑p) z

@[simp]

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

padicValInt p 0 is 0 for any p.

@[simp]

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

padicValInt p 1 is 0 for any p.

@[simp]

theorem padicValInt.of_nat {p n : ℕ} : padicValInt p ↑n = multiplicity p n

The p-adic value of a natural is its p-adic value as an integer.

theorem padicValInt.self {p : ℕ} (hp : 1 < p) : padicValInt p ↑p = 1

If p ≠ 0 and p ≠ 1, then padicValInt p p is 1.

@[simp]

theorem padicValInt.eq_zero_iff {p : ℕ} {z : ℤ} : padicValInt p z = 0 ↔ p = 1 ∨ z = 0 ∨ ¬↑p ∣ z

theorem padicValInt.eq_zero_of_not_dvd {p : ℕ} {z : ℤ} (h : ¬↑p ∣ z) : padicValInt p z = 0

noncomputable def padicValRat (p : ℕ) (q : ℚ) : ℤ

padicValRat defines the valuation of a rational q to be the valuation of q.num minus the valuation of q.den. If q = 0 or p = 1, then padicValRat p q defaults to 0.

Equations

• padicValRat p q = ↑(padicValInt p q.num) - ↑(multiplicity p q.den)

theorem padicValRat_def (p : ℕ) (q : ℚ) : padicValRat p q = ↑(padicValInt p q.num) - ↑(multiplicity p q.den)

@[simp]

theorem padicValRat.neg {p : ℕ} (q : ℚ) : padicValRat p (-q) = padicValRat p q

padicValRat p q is symmetric in q.

@[simp]

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

padicValRat p 0 is 0 for any p.

@[simp]

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

padicValRat p 1 is 0 for any p.

@[simp]

theorem padicValRat.of_int {p : ℕ} {z : ℤ} : padicValRat p ↑z = ↑(padicValInt p z)

The p-adic value of an integer z ≠ 0 is its p-adic value as a rational.

theorem padicValRat.of_int_multiplicity {p : ℕ} {z : ℤ} : padicValRat p ↑z = ↑(multiplicity (↑p) z)

The p-adic value of an integer z ≠ 0 is the multiplicity of p in z.

theorem padicValRat.multiplicity_sub_multiplicity {p : ℕ} {q : ℚ} : padicValRat p q = ↑(multiplicity (↑p) q.num) - ↑(multiplicity p q.den)

@[simp]

theorem padicValRat.of_nat {p n : ℕ} : padicValRat p ↑n = ↑(multiplicity p n)

The p-adic value of an integer z ≠ 0 is its p-adic value as a rational.

theorem padicValRat.self {p : ℕ} (hp : 1 < p) : padicValRat p ↑p = 1

If p ≠ 0 and p ≠ 1, then padicValRat p p is 1.

theorem zero_le_padicValRat_of_nat {p : ℕ} (n : ℕ) : 0 ≤ padicValRat p ↑n

theorem padicValRat_of_nat {p : ℕ} (n : ℕ) : ↑(multiplicity p n) = padicValRat p ↑n

padicValRat coincides with multiplicity.

@[simp]

theorem Nat.Prime.multiplicity_self {p : ℕ} [hp : Fact (Prime p)] : multiplicity p p = 1

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

theorem padicValNat_self {p : ℕ} [hp : Fact (Nat.Prime p)] : multiplicity p p = 1

Alias of Nat.Prime.multiplicity_self.

theorem one_le_multiplicity_of_dvd {p n : ℕ} [hp : Fact (Nat.Prime p)] (hn : n ≠ 0) (div : p ∣ n) : 1 ≤ multiplicity p n

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

theorem one_le_padicValNat_of_dvd {p n : ℕ} [hp : Fact (Nat.Prime p)] (hn : n ≠ 0) (div : p ∣ n) : 1 ≤ multiplicity p n

Alias of one_le_multiplicity_of_dvd.

theorem dvd_iff_multiplicity_ne_zero {p n : ℕ} [Fact (Nat.Prime p)] (hn0 : n ≠ 0) : p ∣ n ↔ multiplicity p n ≠ 0

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

theorem dvd_iff_padicValNat_ne_zero {p n : ℕ} [Fact (Nat.Prime p)] (hn0 : n ≠ 0) : p ∣ n ↔ multiplicity p n ≠ 0

Alias of dvd_iff_multiplicity_ne_zero.

theorem padicValRat.finite_int_prime_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {a : ℤ} : FiniteMultiplicity (↑p) a ↔ a ≠ 0

The multiplicity of p : ℕ in a : ℤ is finite exactly when a ≠ 0.

theorem padicValRat.defn (p : ℕ) [hp : Fact (Nat.Prime p)] {q : ℚ} {n d : ℤ} (hqz : q ≠ 0) (qdf : q = Rat.divInt n d) : padicValRat p q = ↑(multiplicity (↑p) n) - ↑(multiplicity (↑p) d)

A rewrite lemma for padicValRat p q when q is expressed in terms of Rat.mk.

theorem padicValRat.mul {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ} (hq : q ≠ 0) (hr : r ≠ 0) : padicValRat p (q * r) = padicValRat p q + padicValRat p r

A rewrite lemma for padicValRat p (q * r) with conditions q ≠ 0, r ≠ 0.

@[simp]

theorem padicValRat.pow {p : ℕ} [hp : Fact (Nat.Prime p)] (q : ℚ) {k : ℕ} : padicValRat p (q ^ k) = ↑k * padicValRat p q

A rewrite lemma for padicValRat p (q^k).

@[simp]

theorem padicValRat.inv {p : ℕ} [hp : Fact (Nat.Prime p)] (q : ℚ) : padicValRat p q⁻¹ = -padicValRat p q

A rewrite lemma for padicValRat p (q⁻¹).

@[simp]

theorem padicValRat.zpow {p : ℕ} [hp : Fact (Nat.Prime p)] (q : ℚ) {k : ℤ} : padicValRat p (q ^ k) = k * padicValRat p q

theorem padicValRat.div {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ} (hq : q ≠ 0) (hr : r ≠ 0) : padicValRat p (q / r) = padicValRat p q - padicValRat p r

A rewrite lemma for padicValRat p (q / r) with conditions q ≠ 0, r ≠ 0.

theorem padicValRat.padicValRat_le_padicValRat_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {n₁ n₂ d₁ d₂ : ℤ} (hn₁ : n₁ ≠ 0) (hn₂ : n₂ ≠ 0) (hd₁ : d₁ ≠ 0) (hd₂ : d₂ ≠ 0) : padicValRat p (Rat.divInt n₁ d₁) ≤ padicValRat p (Rat.divInt n₂ d₂) ↔ ∀ (n : ℕ), ↑p ^ n ∣ n₁ * d₂ → ↑p ^ n ∣ n₂ * d₁

A condition for padicValRat p (n₁ / d₁) ≤ padicValRat p (n₂ / d₂), in terms of divisibility by p^n.

theorem padicValRat.le_padicValRat_add_of_le {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ} (hqr : q + r ≠ 0) (h : padicValRat p q ≤ padicValRat p r) : padicValRat p q ≤ padicValRat p (q + r)

Sufficient conditions to show that the p-adic valuation of q is less than or equal to the p-adic valuation of q + r.

theorem padicValRat.min_le_padicValRat_add {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ} (hqr : q + r ≠ 0) : min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)

The minimum of the valuations of q and r is at most the valuation of q + r.

theorem padicValRat.add_eq_min {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ} (hqr : q + r ≠ 0) (hq : q ≠ 0) (hr : r ≠ 0) (hval : padicValRat p q ≠ padicValRat p r) : padicValRat p (q + r) = min (padicValRat p q) (padicValRat p r)

Ultrametric property of a p-adic valuation.

theorem padicValRat.add_eq_of_lt {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ} (hqr : q + r ≠ 0) (hq : q ≠ 0) (hr : r ≠ 0) (hval : padicValRat p q < padicValRat p r) : padicValRat p (q + r) = padicValRat p q

theorem padicValRat.lt_add_of_lt {p : ℕ} [hp : Fact (Nat.Prime p)] {q r₁ r₂ : ℚ} (hqr : r₁ + r₂ ≠ 0) (hval₁ : padicValRat p q < padicValRat p r₁) (hval₂ : padicValRat p q < padicValRat p r₂) : padicValRat p q < padicValRat p (r₁ + r₂)

theorem padicValRat.self_pow_inv {p : ℕ} [hp : Fact (Nat.Prime p)] (r : ℕ) : padicValRat p (↑p ^ r)⁻¹ = -↑r

theorem padicValRat.sum_pos_of_pos {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} {F : ℕ → ℚ} (hF : ∀ i < n, 0 < padicValRat p (F i)) (hn0 : ∑ i ∈ Finset.range n, F i ≠ 0) : 0 < padicValRat p (∑ i ∈ Finset.range n, F i)

A finite sum of rationals with positive p-adic valuation has positive p-adic valuation (if the sum is non-zero).

theorem padicValRat.lt_sum_of_lt {p j : ℕ} [hp : Fact (Nat.Prime p)] {F : ℕ → ℚ} {S : Finset ℕ} (hS : S.Nonempty) (hF : ∀ i ∈ S, padicValRat p (F j) < padicValRat p (F i)) (hn1 : ∀ (i : ℕ), 0 < F i) : padicValRat p (F j) < padicValRat p (∑ i ∈ S, F i)

If the p-adic valuation of a finite set of positive rationals is greater than a given rational number, then the p-adic valuation of their sum is also greater than the same rational number.

theorem Rat.num_or_den_zero_padicVal (a : ℚ) {p : ℕ} (hp : Nat.Prime p) : padicValInt p a.num = 0 ∨ multiplicity p a.den = 0

The numerator or denominator of a rational number has zero p-adic valuation.

theorem Rat.num_den_even_padicVal_of_even_padicVal {a : ℚ} {p : ℕ} (hp : Nat.Prime p) (h : Even (padicValRat p a)) : Even (padicValInt p a.num) ∧ Even (multiplicity p a.den)

The numerator and denominator of a rational number with even p-adic valuation also have even p-adic valuation.

theorem Rat.isSquare_iff_even_factorization {a : ℚ} : IsSquare a ↔ 0 ≤ a ∧ ∀ (p : ℕ), Nat.Prime p → Even (padicValRat p a)

A rational number is a square if and only if it is nonnegative, and has even p-adic valuation for all p.

theorem Nat.multiplicity_mul {p a b : ℕ} [hp : Fact (Prime p)] : a ≠ 0 → b ≠ 0 → multiplicity p (a * b) = multiplicity p a + multiplicity p b

A rewrite lemma for multiplicity p (a * b) with conditions a ≠ 0, b ≠ 0.

theorem Nat.multiplicity_div_of_dvd {p a b : ℕ} [hp : Fact (Prime p)] (h : b ∣ a) : multiplicity p (a / b) = multiplicity p a - multiplicity p b

theorem Nat.multiplicity_div {p b : ℕ} [hp : Fact (Prime p)] (dvd : p ∣ b) : multiplicity p (b / p) = multiplicity p b - 1

Dividing out by a prime factor reduces the multiplicity by 1.

@[simp]

theorem Nat.multiplicity_pow {p : ℕ} [hp : Fact (Prime p)] (a n : ℕ) : multiplicity p (a ^ n) = n * multiplicity p a

A version of padicValRat.pow for multiplicity.

theorem Nat.multiplicity_prime_pow {p : ℕ} [hp : Fact (Prime p)] (n : ℕ) : multiplicity p (p ^ n) = n

theorem Nat.multiplicity_div_pow {p a b : ℕ} [hp : Fact (Prime p)] (dvd : p ^ a ∣ b) : multiplicity p (b / p ^ a) = multiplicity p b - a

theorem Nat.multiplicity_div' {p : ℕ} [hp : Fact (Prime p)] {m : ℕ} (cpm : p.Coprime m) {b : ℕ} (dvd : m ∣ b) : multiplicity p (b / m) = multiplicity p b

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

theorem padicValNat.mul {p a b : ℕ} [hp : Fact (Nat.Prime p)] : a ≠ 0 → b ≠ 0 → multiplicity p (a * b) = multiplicity p a + multiplicity p b

Alias of Nat.multiplicity_mul.

---

A rewrite lemma for multiplicity p (a * b) with conditions a ≠ 0, b ≠ 0.

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

theorem padicValNat.div_of_dvd {p a b : ℕ} [hp : Fact (Nat.Prime p)] (h : b ∣ a) : multiplicity p (a / b) = multiplicity p a - multiplicity p b

Alias of Nat.multiplicity_div_of_dvd.

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

theorem padicValNat.div {p b : ℕ} [hp : Fact (Nat.Prime p)] (dvd : p ∣ b) : multiplicity p (b / p) = multiplicity p b - 1

Alias of Nat.multiplicity_div.

---

Dividing out by a prime factor reduces the multiplicity by 1.

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

theorem padicValNat.pow {p : ℕ} [hp : Fact (Nat.Prime p)] (a n : ℕ) : multiplicity p (a ^ n) = n * multiplicity p a

Alias of Nat.multiplicity_pow.

---

A version of padicValRat.pow for multiplicity.

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

theorem padicValNat.prime_pow {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) : multiplicity p (p ^ n) = n

Alias of Nat.multiplicity_prime_pow.

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

theorem padicValNat.div_pow {p a b : ℕ} [hp : Fact (Nat.Prime p)] (dvd : p ^ a ∣ b) : multiplicity p (b / p ^ a) = multiplicity p b - a

Alias of Nat.multiplicity_div_pow.

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

theorem padicValNat.div' {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (cpm : p.Coprime m) {b : ℕ} (dvd : m ∣ b) : multiplicity p (b / m) = multiplicity p b

Alias of Nat.multiplicity_div'.

theorem dvd_of_one_le_multiplicity {p n : ℕ} (hp : 1 ≤ multiplicity p n) : p ∣ n

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

theorem dvd_of_one_le_padicValNat {p n : ℕ} (hp : 1 ≤ multiplicity p n) : p ∣ n

Alias of dvd_of_one_le_multiplicity.

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

theorem padicValNat_dvd_iff_le_of_ne_one {p k n : ℕ} (hp : p ≠ 1) (hn : n ≠ 0) : p ^ k ∣ n ↔ k ≤ multiplicity p n

Alias of Nat.pow_dvd_iff_le_multiplicity.

theorem multiplicity_dvd_iff_le {p : ℕ} [hp : Fact (Nat.Prime p)] {a n : ℕ} (ha : a ≠ 0) : p ^ n ∣ a ↔ n ≤ multiplicity p a

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

theorem padicValNat_dvd_iff_le {p : ℕ} [hp : Fact (Nat.Prime p)] {a n : ℕ} (ha : a ≠ 0) : p ^ n ∣ a ↔ n ≤ multiplicity p a

Alias of multiplicity_dvd_iff_le.

theorem multiplicity_dvd_iff_of_ne_one {p : ℕ} (hp : p ≠ 1) (n a : ℕ) : p ^ n ∣ a ↔ a = 0 ∨ n ≤ multiplicity p a

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

theorem padicValNat_dvd_iff_of_ne_one {p : ℕ} (hp : p ≠ 1) (n a : ℕ) : p ^ n ∣ a ↔ a = 0 ∨ n ≤ multiplicity p a

Alias of multiplicity_dvd_iff_of_ne_one.

theorem multiplicity_dvd_iff {p : ℕ} (n : ℕ) [hp : Fact (Nat.Prime p)] (a : ℕ) : p ^ n ∣ a ↔ a = 0 ∨ n ≤ multiplicity p a

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

theorem padicValNat_dvd_iff {p : ℕ} (n : ℕ) [hp : Fact (Nat.Prime p)] (a : ℕ) : p ^ n ∣ a ↔ a = 0 ∨ n ≤ multiplicity p a

Alias of multiplicity_dvd_iff.

theorem pow_succ_multiplicity_not_dvd {p n : ℕ} [hp : Fact (Nat.Prime p)] (hn : n ≠ 0) : ¬p ^ (multiplicity p n + 1) ∣ n

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

theorem pow_succ_padicValNat_not_dvd {p n : ℕ} [hp : Fact (Nat.Prime p)] (hn : n ≠ 0) : ¬p ^ (multiplicity p n + 1) ∣ n

Alias of pow_succ_multiplicity_not_dvd.

theorem multiplicity_primes {p q : ℕ} [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (ne : p ≠ q) : multiplicity p q = 0

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

theorem padicValNat_primes {p q : ℕ} [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (ne : p ≠ q) : multiplicity p q = 0

Alias of multiplicity_primes.

theorem multiplicity_prime_prime_pow {p q : ℕ} [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (n : ℕ) (ne : p ≠ q) : multiplicity p (q ^ n) = 0

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

theorem padicValNat_prime_prime_pow {p q : ℕ} [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (n : ℕ) (ne : p ≠ q) : multiplicity p (q ^ n) = 0

Alias of multiplicity_prime_prime_pow.

theorem multiplicity_mul_pow_left {p q : ℕ} [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (n m : ℕ) (ne : p ≠ q) : multiplicity p (p ^ n * q ^ m) = n

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

theorem padicValNat_mul_pow_left {p q : ℕ} [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (n m : ℕ) (ne : p ≠ q) : multiplicity p (p ^ n * q ^ m) = n

Alias of multiplicity_mul_pow_left.

theorem multiplicity_mul_pow_right {p q : ℕ} [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (n m : ℕ) (ne : q ≠ p) : multiplicity q (p ^ n * q ^ m) = m

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

theorem padicValNat_mul_pow_right {p q : ℕ} [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (n m : ℕ) (ne : q ≠ p) : multiplicity q (p ^ n * q ^ m) = m

Alias of multiplicity_mul_pow_right.

theorem multiplicity_le_nat_log {p : ℕ} (n : ℕ) : multiplicity p n ≤ Nat.log p n

The p-adic valuation of n is less than or equal to its logarithm w.r.t. p.

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

theorem padicValNat_le_nat_log {p : ℕ} (n : ℕ) : multiplicity p n ≤ Nat.log p n

Alias of multiplicity_le_nat_log.

---

The p-adic valuation of n is less than or equal to its logarithm w.r.t. p.

theorem multiplicity_add_le_self {p a : ℕ} [hp : Fact (Nat.Prime p)] (ha : p < a) : multiplicity p a + p ≤ a

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

theorem padicValNat_add_le_self {p a : ℕ} [hp : Fact (Nat.Prime p)] (ha : p < a) : multiplicity p a + p ≤ a

Alias of multiplicity_add_le_self.

theorem nat_log_eq_multiplicity_iff {p n : ℕ} [hp : Fact (Nat.Prime p)] (hn : n ≠ 0) : Nat.log p n = multiplicity p n ↔ n < p ^ (multiplicity p n + 1)

The p-adic valuation of n is equal to the logarithm w.r.t. p iff n is less than p raised to one plus the p-adic valuation of n.

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

theorem nat_log_eq_padicValNat_iff {p n : ℕ} [hp : Fact (Nat.Prime p)] (hn : n ≠ 0) : Nat.log p n = multiplicity p n ↔ n < p ^ (multiplicity p n + 1)

Alias of nat_log_eq_multiplicity_iff.

---

The p-adic valuation of n is equal to the logarithm w.r.t. p iff n is less than p raised to one plus the p-adic valuation of n.

theorem Nat.log_ne_multiplicity_succ {n : ℕ} (hn : n ≠ 0) : log 2 n ≠ multiplicity 2 (n + 1)

This is false for prime numbers other than 2: for p = 3, n = 1, one has log 3 1 = multiplicity 3 2 = 0.

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

theorem Nat.log_ne_padicValNat_succ {n : ℕ} (hn : n ≠ 0) : log 2 n ≠ multiplicity 2 (n + 1)

Alias of Nat.log_ne_multiplicity_succ.

---

This is false for prime numbers other than 2: for p = 3, n = 1, one has log 3 1 = multiplicity 3 2 = 0.

theorem Nat.max_log_multiplicity_succ_eq_log_succ {p : ℕ} (n : ℕ) [hp : Fact (Prime p)] : max (log p n) (multiplicity p (n + 1)) = log p (n + 1)

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

theorem Nat.max_log_padicValNat_succ_eq_log_succ {p : ℕ} (n : ℕ) [hp : Fact (Prime p)] : max (log p n) (multiplicity p (n + 1)) = log p (n + 1)

Alias of Nat.max_log_multiplicity_succ_eq_log_succ.

theorem range_pow_multiplicity_subset_divisors {p n : ℕ} (hn : n ≠ 0) : Finset.image (fun (x : ℕ) => p ^ x) (Finset.range (multiplicity p n + 1)) ⊆ n.divisors

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

theorem range_pow_padicValNat_subset_divisors {p n : ℕ} (hn : n ≠ 0) : Finset.image (fun (x : ℕ) => p ^ x) (Finset.range (multiplicity p n + 1)) ⊆ n.divisors

Alias of range_pow_multiplicity_subset_divisors.

theorem range_pow_multiplicity_subset_divisors' {p n : ℕ} [hp : Fact (Nat.Prime p)] : Finset.image (fun (t : ℕ) => p ^ (t + 1)) (Finset.range (multiplicity p n)) ⊆ n.divisors.erase 1

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

theorem range_pow_padicValNat_subset_divisors' {p n : ℕ} [hp : Fact (Nat.Prime p)] : Finset.image (fun (t : ℕ) => p ^ (t + 1)) (Finset.range (multiplicity p n)) ⊆ n.divisors.erase 1

Alias of range_pow_multiplicity_subset_divisors'.

theorem multiplicity_factorial_mul {p : ℕ} (n : ℕ) [hp : Fact (Nat.Prime p)] : multiplicity p (p * n).factorial = multiplicity p n.factorial + n

The p-adic valuation of (p * n)! is n more than that of n!.

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

theorem padicValNat_factorial_mul {p : ℕ} (n : ℕ) [hp : Fact (Nat.Prime p)] : multiplicity p (p * n).factorial = multiplicity p n.factorial + n

Alias of multiplicity_factorial_mul.

---

The p-adic valuation of (p * n)! is n more than that of n!.

theorem multiplicity_eq_zero_of_mem_Ioo {p m k : ℕ} (hm : m ∈ Set.Ioo (p * k) (p * (k + 1))) : multiplicity p m = 0

The p-adic valuation of m equals zero if it is between p * k and p * (k + 1) for some k.

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

theorem padicValNat_eq_zero_of_mem_Ioo {p m k : ℕ} (hm : m ∈ Set.Ioo (p * k) (p * (k + 1))) : multiplicity p m = 0

Alias of multiplicity_eq_zero_of_mem_Ioo.

---

The p-adic valuation of m equals zero if it is between p * k and p * (k + 1) for some k.

theorem multiplicity_factorial_mul_add {p n : ℕ} (m : ℕ) [hp : Fact (Nat.Prime p)] (h : n < p) : multiplicity p (p * m + n).factorial = multiplicity p (p * m).factorial

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

theorem padicValNat_factorial_mul_add {p n : ℕ} (m : ℕ) [hp : Fact (Nat.Prime p)] (h : n < p) : multiplicity p (p * m + n).factorial = multiplicity p (p * m).factorial

Alias of multiplicity_factorial_mul_add.

@[simp]

theorem multiplicity_mul_div_factorial {p : ℕ} (n : ℕ) [hp : Fact (Nat.Prime p)] : multiplicity p (p * (n / p)).factorial = multiplicity p n.factorial

The p-adic valuation of n! is equal to the p-adic valuation of the factorial of the largest multiple of p below n, i.e. (p * ⌊n / p⌋)!.

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

theorem padicValNat_mul_div_factorial {p : ℕ} (n : ℕ) [hp : Fact (Nat.Prime p)] : multiplicity p (p * (n / p)).factorial = multiplicity p n.factorial

Alias of multiplicity_mul_div_factorial.

---

The p-adic valuation of n! is equal to the p-adic valuation of the factorial of the largest multiple of p below n, i.e. (p * ⌊n / p⌋)!.

theorem multiplicity_factorial {p n b : ℕ} [hp : Fact (Nat.Prime p)] (hnb : Nat.log p n < b) : multiplicity p n.factorial = ∑ i ∈ Finset.Ico 1 b, n / p ^ i

Legendre's Theorem

The p-adic valuation of n! is the sum of the quotients n / p ^ i. This sum is expressed over the finset Ico 1 b where b is any bound greater than log p n.

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

theorem padicValNat_factorial {p n b : ℕ} [hp : Fact (Nat.Prime p)] (hnb : Nat.log p n < b) : multiplicity p n.factorial = ∑ i ∈ Finset.Ico 1 b, n / p ^ i

Alias of multiplicity_factorial.

---

Legendre's Theorem

The p-adic valuation of n! is the sum of the quotients n / p ^ i. This sum is expressed over the finset Ico 1 b where b is any bound greater than log p n.

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

theorem sub_one_mul_padicValNat_factorial {n p : ℕ} (hp : Nat.Prime p) : (p - 1) * multiplicity p n.factorial = n - (p.digits n).sum

Alias of Nat.Prime.sub_one_mul_multiplicity_factorial.

theorem sub_one_mul_multiplicity_factorial_lt_of_ne_zero (p : ℕ) [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : n ≠ 0) : (p - 1) * multiplicity p n.factorial < n

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

theorem sub_one_mul_padicValNat_factorial_lt_of_ne_zero (p : ℕ) [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : n ≠ 0) : (p - 1) * multiplicity p n.factorial < n

Alias of sub_one_mul_multiplicity_factorial_lt_of_ne_zero.

theorem multiplicity_factorial_lt_of_ne_zero (p : ℕ) [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : n ≠ 0) : multiplicity p n.factorial < n

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

theorem padicValNat_factorial_lt_of_ne_zero (p : ℕ) [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : n ≠ 0) : multiplicity p n.factorial < n

Alias of multiplicity_factorial_lt_of_ne_zero.

theorem multiplicity_factorial_le (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : multiplicity p n.factorial ≤ n

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

theorem padicValNat_factorial_le (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : multiplicity p n.factorial ≤ n

Alias of multiplicity_factorial_le.

theorem multiplicity_choose {p n k b : ℕ} [hp : Fact (Nat.Prime p)] (hkn : k ≤ n) (hnb : Nat.log p n < b) : multiplicity p (n.choose k) = {i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i}.card

Kummer's Theorem

The p-adic valuation of n.choose k is the number of carries when k and n - k are added in base p. This sum is expressed over the finset Ico 1 b where b is any bound greater than log p n.

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

theorem padicValNat_choose {p n k b : ℕ} [hp : Fact (Nat.Prime p)] (hkn : k ≤ n) (hnb : Nat.log p n < b) : multiplicity p (n.choose k) = {i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i}.card

Alias of multiplicity_choose.

---

Kummer's Theorem

The p-adic valuation of n.choose k is the number of carries when k and n - k are added in base p. This sum is expressed over the finset Ico 1 b where b is any bound greater than log p n.

theorem multiplicity_choose' {p n k b : ℕ} [hp : Fact (Nat.Prime p)] (hnb : Nat.log p (n + k) < b) : multiplicity p ((n + k).choose k) = {i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}.card

Kummer's Theorem

The p-adic valuation of (n + k).choose k is the number of carries when k and n are added in base p. This sum is expressed over the finset Ico 1 b where b is any bound greater than log p (n + k).

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

theorem padicValNat_choose' {p n k b : ℕ} [hp : Fact (Nat.Prime p)] (hnb : Nat.log p (n + k) < b) : multiplicity p ((n + k).choose k) = {i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}.card

Alias of multiplicity_choose'.

---

Kummer's Theorem

The p-adic valuation of (n + k).choose k is the number of carries when k and n are added in base p. This sum is expressed over the finset Ico 1 b where b is any bound greater than log p (n + k).

theorem sub_one_mul_multiplicity_choose_eq_sub_sum_digits' {p k n : ℕ} [hp : Fact (Nat.Prime p)] : (p - 1) * multiplicity p ((n + k).choose k) = (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum

Kummer's Theorem Taking (p - 1) times the p-adic valuation of the binomial n + k over k equals the sum of the digits of k plus the sum of the digits of n minus the sum of digits of n + k, all base p.

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

theorem sub_one_mul_padicValNat_choose_eq_sub_sum_digits' {p k n : ℕ} [hp : Fact (Nat.Prime p)] : (p - 1) * multiplicity p ((n + k).choose k) = (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum

Alias of sub_one_mul_multiplicity_choose_eq_sub_sum_digits'.

---

Kummer's Theorem Taking (p - 1) times the p-adic valuation of the binomial n + k over k equals the sum of the digits of k plus the sum of the digits of n minus the sum of digits of n + k, all base p.

theorem sub_one_mul_multiplicity_choose_eq_sub_sum_digits {p k n : ℕ} [hp : Fact (Nat.Prime p)] (h : k ≤ n) : (p - 1) * multiplicity p (n.choose k) = (p.digits k).sum + (p.digits (n - k)).sum - (p.digits n).sum

Kummer's Theorem Taking (p - 1) times the p-adic valuation of the binomial n over k equals the sum of the digits of k plus the sum of the digits of n - k minus the sum of digits of n, all base p.

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

theorem sub_one_mul_padicValNat_choose_eq_sub_sum_digits {p k n : ℕ} [hp : Fact (Nat.Prime p)] (h : k ≤ n) : (p - 1) * multiplicity p (n.choose k) = (p.digits k).sum + (p.digits (n - k)).sum - (p.digits n).sum

Alias of sub_one_mul_multiplicity_choose_eq_sub_sum_digits.

---

Kummer's Theorem Taking (p - 1) times the p-adic valuation of the binomial n over k equals the sum of the digits of k plus the sum of the digits of n - k minus the sum of digits of n, all base p.

theorem padicValInt_dvd_iff_of_ne_one {p : ℕ} (hp : p ≠ 1) (n : ℕ) (a : ℤ) : ↑p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValInt p a

theorem padicValInt_dvd_iff {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) (a : ℤ) : ↑p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValInt p a

theorem padicValInt_dvd {p : ℕ} (a : ℤ) : ↑p ^ padicValInt p a ∣ a

theorem padicValInt_self {p : ℕ} [hp : Fact (Nat.Prime p)] : padicValInt p ↑p = 1

theorem padicValInt.mul {p : ℕ} [hp : Fact (Nat.Prime p)] {a b : ℤ} (ha : a ≠ 0) (hb : b ≠ 0) : padicValInt p (a * b) = padicValInt p a + padicValInt p b

theorem padicValInt_mul_eq_succ {p : ℕ} [hp : Fact (Nat.Prime p)] (a : ℤ) (ha : a ≠ 0) : padicValInt p (a * ↑p) = padicValInt p a + 1