The maximal power of one natural number dividing another #

Here we introduce p.maxPowDvd n which returns the maximal k : ℕ for which p ^ k ∣ n with the convention that maxPowDvd 1 n = 0 for all n.

We prove enough about maxPowDvd in this file to show equality with Nat.padicValNat in padicValNat.padicValNat_eq_maxPowDvd.

The implementation of maxPowDvd improves on the speed of padicValNat.

source

def Nat.maxPowDvdDiv (p n : ℕ) :

ℕ × ℕ

Find largest k : ℕ such that p ^ k ∣ n for any p : ℕ, as well as the ratio n / p ^ k.

The implementation recurses from (p, n) to (p * p, n), so the recursion depth is $$O(\log(\nu_p(n)))$$, thus it is $$O(\log(\log(n)))$$.

Equations

p.maxPowDvdDiv n = if H : 1 < p ∧ n ≠ 0 then Nat.maxPowDvdDiv.go n p H else (0, n)

Instances For

source

@[irreducible]

def Nat.maxPowDvdDiv.go (n p : ℕ) (hp : 1 < p ∧ n ≠ 0) :

ℕ × ℕ

Auxiliary definition for Nat.maxPowDvdDiv.

Equations

Nat.maxPowDvdDiv.go n p hp = if hmod : n % p = 0 then match Nat.maxPowDvdDiv.go n (p * p) ⋯ with | (e, q) => if q % p = 0 then (2 * e + 1, q / p) else (2 * e, q) else (0, n)

Instances For

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

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

Instances For

source

def Nat.divMaxPow (n p : ℕ) :

ℕ

Divide n by the maximal power of p that divides n.

Equations

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

Instances For

source

theorem Nat.maxPowDvdDiv.go_spec {n p : ℕ} (hnp : 1 < p ∧ n ≠ 0) :

(go n p hnp).snd * p ^ (go n p hnp).fst = n ∧ ¬p ∣ (go n p hnp).snd

source

theorem Nat.maxPowDvdDiv_of_base_le_one {p : ℕ} (hp : p ≤ 1) (n : ℕ) :

p.maxPowDvdDiv n = (0, n)

source

@[simp]

theorem Nat.maxPowDvdDiv_zero_left (n : ℕ) :

maxPowDvdDiv 0 n = (0, n)

source

@[simp]

theorem padicValNat_zero_left (n : ℕ) :

padicValNat 0 n = 0

source

@[simp]

theorem Nat.divMaxPow_zero_right (n : ℕ) :

n.divMaxPow 0 = n

source

@[simp]

theorem Nat.maxPowDvdDiv_one_left (n : ℕ) :

maxPowDvdDiv 1 n = (0, n)

source

@[simp]

theorem padicValNat_one_left (n : ℕ) :

padicValNat 1 n = 0

source

@[simp]

theorem Nat.divMaxPow_one_right (n : ℕ) :

n.divMaxPow 1 = n

source

@[simp]

theorem Nat.maxPowDvdDiv_zero_right (p : ℕ) :

p.maxPowDvdDiv 0 = (0, 0)

source

@[simp]

theorem padicValNat_zero_right (p : ℕ) :

padicValNat p 0 = 0

source

@[simp]

theorem Nat.divMaxPow_zero_left (p : ℕ) :

divMaxPow 0 p = 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.divMaxPow_mul_pow_padicValNat (p n : ℕ) :

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

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.not_dvd_divMaxPow {p n : ℕ} (hp : 1 < p) (hn : n ≠ 0) :

¬p ∣ n.divMaxPow p

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

source

@[simp]

theorem Nat.snd_maxPowDvdDiv (p n : ℕ) :

(p.maxPowDvdDiv n).snd = 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