The p-adic valuation on natural numbers #

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

padicValNat p n = (p.maxPowDvdDiv n).1

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

@[simp]

theorem padicValNat_zero_left (n : ℕ) :

padicValNat 0 n = 0

source

@[simp]

theorem padicValNat_one_left (n : ℕ) :

padicValNat 1 n = 0

source

@[simp]

theorem padicValNat_zero_right (p : ℕ) :

padicValNat p 0 = 0

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

@[simp]

theorem padicValNat_one_right (p : ℕ) :

padicValNat p 1 = 0

source

@[simp]

theorem Nat.divMaxPow_one_left (p : ℕ) :

divMaxPow 1 p = 1

source

@[simp]

theorem Nat.pow_padicValNat_mul_divMaxPow (p n : ℕ) :

p ^ padicValNat p n * n.divMaxPow p = n

source

theorem pow_padicValNat_dvd {p n : ℕ} :

p ^ padicValNat p n ∣ n

source

theorem Nat.padicValNat_lt_self {p n : ℕ} (hn : n ≠ 0) :

padicValNat p n < n

source

theorem Nat.padicValNat_le_self {p : ℕ} (n : ℕ) :

padicValNat p n ≤ n

source

theorem Nat.pow_dvd_iff_le_padicValNat {p k n : ℕ} (hp : p ≠ 1) (hn : n ≠ 0) :

p ^ k ∣ n ↔ k ≤ padicValNat p n

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) = (padicValNat p n + k, n.divMaxPow p)

source

@[simp]

theorem padicValNat_base_pow_mul {p n : ℕ} (hp : 1 < p) (hn : n ≠ 0) (k : ℕ) :

padicValNat p (p ^ k * n) = padicValNat p n + k

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) = (padicValNat p n + 1, n.divMaxPow p)

source

@[simp]

theorem padicValNat_base_mul {p n : ℕ} (hp : 1 < p) (hn : n ≠ 0) :

padicValNat p (p * n) = padicValNat p n + 1

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 padicValNat_base_pow {p : ℕ} (hp : 1 < p) (k : ℕ) :

padicValNat p (p ^ k) = k

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 padicValNat_base {p : ℕ} (hp : 1 < p) :

padicValNat p p = 1

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 = padicValNat p n

source

@[simp]

theorem Nat.snd_maxPowDvdDiv (p n : ℕ) :

(p.maxPowDvdDiv n).2 = n.divMaxPow p

source

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

def Nat.maxPowDiv (p n : ℕ) :

ℕ

Alias of padicValNat.

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