Documentation

Mathlib.Data.Nat.PadicValNat

The p-adic valuation on natural numbers #

source
def padicValNat (p n : ℕ) :
ℕ

For p ≠ 1, the p-adic valuation of a natural n ≠ 0 is the largest natural number k such that p^k divides n. If n = 0 or p = 1, then padicValNat p n defaults to 0.

Equations
Instances For
    source
    @[simp]
    theorem Nat.divMaxPow_mul_pow_padicValNat (p n : ℕ) :
    n.divMaxPow p * p ^ padicValNat p n = n
    source
    theorem Nat.padicValNat_def {p n : ℕ} :
    padicValNat p n = multiplicity p n
    source
    @[deprecated multiplicity_zero_left (since := "2026-10-28")]
    theorem padicValNat_zero_left {α : Type u_1} [MonoidWithZero α] (a : α) :
    multiplicity 0 a = 0

    Alias of multiplicity_zero_left.

    source
    @[deprecated multiplicity_one_left (since := "2026-10-28")]
    theorem padicValNat_one_left {α : Type u_1} [Monoid α] (b : α) :
    multiplicity 1 b = 0

    Alias of multiplicity_one_left.

    source
    @[deprecated multiplicity_zero_right (since := "2026-10-28")]
    theorem padicValNat_zero_right {α : Type u_1} [MonoidWithZero α] (a : α) :
    multiplicity a 0 = 0

    Alias of multiplicity_zero_right.

    source
    theorem Nat.maxPowDvdDiv_of_not_dvd {p n : ℕ} (h : ¬p ∣ n) :
    p.maxPowDvdDiv n = (0, n)
    source
    @[simp]
    theorem Nat.maxPowDvdDiv_one_right (p : ℕ) :
    p.maxPowDvdDiv 1 = (0, 1)
    source
    @[deprecated multiplicity_one_right (since := "2026-10-28")]
    theorem padicValNat_one_right {α : Type u_1} [Monoid α] {a : α} :
    multiplicity a 1 = 0

    Alias of multiplicity_one_right.

    source
    @[simp]
    theorem Nat.divMaxPow_one_left (p : ℕ) :
    divMaxPow 1 p = 1
    source
    @[simp]
    theorem Nat.pow_multiplicity_mul_divMaxPow (p n : ℕ) :
    p ^ multiplicity p n * n.divMaxPow p = n
    source
    @[deprecated Nat.pow_multiplicity_mul_divMaxPow (since := "2026-10-28")]
    theorem Nat.pow_padicValNat_mul_divMaxPow (p n : ℕ) :
    p ^ multiplicity p n * n.divMaxPow p = n

    Alias of Nat.pow_multiplicity_mul_divMaxPow.

    source
    @[deprecated pow_multiplicity_dvd (since := "2026-10-28")]
    theorem pow_padicValNat_dvd {α : Type u_1} [Monoid α] (a b : α) :
    a ^ multiplicity a b ∣ b

    Alias of pow_multiplicity_dvd.

    source
    theorem Nat.multiplicity_lt_self {p n : ℕ} (hn : n ≠ 0) :
    multiplicity p n < n
    source
    @[deprecated Nat.multiplicity_lt_self (since := "2026-10-28")]
    theorem Nat.padicValNat_lt_self {p n : ℕ} (hn : n ≠ 0) :
    multiplicity p n < n

    Alias of Nat.multiplicity_lt_self.

    source
    theorem Nat.multiplicity_le_self {p : ℕ} (n : ℕ) :
    multiplicity p n ≤ n
    source
    @[deprecated Nat.multiplicity_le_self (since := "2026-10-28")]
    theorem Nat.padicValNat_le_self {p : ℕ} (n : ℕ) :
    multiplicity p n ≤ n

    Alias of Nat.multiplicity_le_self.

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

    If p > 1, n > 0, then the first component of maxPowDvdDiv is the maximal power of p that divides n.

    source
    @[deprecated Nat.pow_dvd_iff_le_multiplicity (since := "2026-10-28")]
    theorem Nat.pow_dvd_iff_le_padicValNat {p k n : ℕ} (hp : p ≠ 1) (hn : n ≠ 0) :
    p ^ k ∣ n ↔ k ≤ multiplicity p n

    Alias of Nat.pow_dvd_iff_le_multiplicity.

    If p > 1, n > 0, then the first component of maxPowDvdDiv is the maximal power of p that divides n.

    source
    theorem Nat.maxPowDvdDiv_of_pow_mul_eq {p n k l : ℕ} (hn : n ≠ 0) (h : p ^ k * l = n) (hl : ¬p ∣ l) :
    p.maxPowDvdDiv n = (k, l)
    source
    @[simp]
    theorem Nat.maxPowDvdDiv_base_pow_mul {p n : ℕ} (hp : 1 < p) (hn : n ≠ 0) (k : ℕ) :
    p.maxPowDvdDiv (p ^ k * n) = (multiplicity p n + k, n.divMaxPow p)
    source
    @[simp]
    theorem multiplicity_base_pow_mul {p n : ℕ} (hp : 1 < p) (hn : n ≠ 0) (k : ℕ) :
    multiplicity p (p ^ k * n) = multiplicity p n + k
    source
    @[deprecated multiplicity_base_pow_mul (since := "2026-10-28")]
    theorem padicValNat_base_pow_mul {p n : ℕ} (hp : 1 < p) (hn : n ≠ 0) (k : ℕ) :
    multiplicity p (p ^ k * n) = multiplicity p n + k

    Alias of multiplicity_base_pow_mul.

    source
    @[simp]
    theorem Nat.divMaxPow_base_pow_mul {p : ℕ} (hp : p ≠ 0) (n k : ℕ) :
    (p ^ k * n).divMaxPow p = n.divMaxPow p
    source
    @[simp]
    theorem Nat.maxPowDvdDiv_base_mul {p n : ℕ} (hp : 1 < p) (hn : n ≠ 0) :
    p.maxPowDvdDiv (p * n) = (multiplicity p n + 1, n.divMaxPow p)
    source
    @[simp]
    theorem multiplicity_base_mul {p n : ℕ} (hp : 1 < p) (hn : n ≠ 0) :
    multiplicity p (p * n) = multiplicity p n + 1
    source
    @[deprecated multiplicity_base_mul (since := "2026-10-28")]
    theorem padicValNat_base_mul {p n : ℕ} (hp : 1 < p) (hn : n ≠ 0) :
    multiplicity p (p * n) = multiplicity p n + 1

    Alias of multiplicity_base_mul.

    source
    @[simp]
    theorem Nat.divMaxPow_base_mul {p : ℕ} (hp : p ≠ 0) (n : ℕ) :
    (p * n).divMaxPow p = n.divMaxPow p
    source
    @[simp]
    theorem Nat.maxPowDvdDiv_base_pow {p : ℕ} (hp : 1 < p) (k : ℕ) :
    p.maxPowDvdDiv (p ^ k) = (k, 1)
    source
    @[simp]
    theorem multiplicity_base_pow {p : ℕ} (hp : 1 < p) (k : ℕ) :
    multiplicity p (p ^ k) = k
    source
    @[deprecated multiplicity_base_pow (since := "2026-10-28")]
    theorem padicValNat_base_pow {p : ℕ} (hp : 1 < p) (k : ℕ) :
    multiplicity p (p ^ k) = k

    Alias of multiplicity_base_pow.

    source
    @[simp]
    theorem Nat.divMaxPow_base_pow {p : ℕ} (hp : p ≠ 0) (k : ℕ) :
    (p ^ k).divMaxPow p = 1
    source
    @[simp]
    theorem Nat.maxPowDvdDiv_self {p : ℕ} (hp : 1 < p) :
    p.maxPowDvdDiv p = (1, 1)
    source
    @[simp]
    theorem Nat.multiplicity_self {p : ℕ} (hp : 1 < p) :
    multiplicity p p = 1
    source
    @[deprecated Nat.multiplicity_self (since := "2026-10-28")]
    theorem padicValNat_base {p : ℕ} (hp : 1 < p) :
    multiplicity p p = 1

    Alias of Nat.multiplicity_self.

    source
    @[simp]
    theorem Nat.divMaxPow_self {p : ℕ} (hp : p ≠ 0) :
    p.divMaxPow p = 1
    source
    @[simp]
    theorem Nat.fst_maxPowDvdDiv (p n : ℕ) :
    (p.maxPowDvdDiv n).1 = multiplicity p n
    source
    @[simp]
    theorem Nat.snd_maxPowDvdDiv (p n : ℕ) :
    (p.maxPowDvdDiv n).2 = n.divMaxPow p