The maximal power of one natural number dividing another

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

We prove enough about maxPowDiv in this file to show equality with Nat.padicValNat in padicValNat.padicValNat_eq_maxPowDiv.

The implementation of maxPowDiv improves on the speed of padicValNat.

def Nat.maxPowDiv (p : ℕ) (n : ℕ) : ℕ

Tail recursive function which returns the largest k : ℕ such that p ^ k ∣ n for any p : ℕ. padicValNat_eq_maxPowDiv allows the code generator to use this definition for padicValNat

Equations

• p.maxPowDiv n = Nat.maxPowDiv.go 0 p n

def Nat.maxPowDiv.go (k : ℕ) (p : ℕ) (n : ℕ) : ℕ

Tail recursive function which returns the largest k : ℕ such that p ^ k ∣ n for any p : ℕ. padicValNat_eq_maxPowDiv allows the code generator to use this definition for padicValNat

Equations

• Nat.maxPowDiv.go k p n = if h : 1 < p ∧ 0 < n ∧ n % p = 0 then let_fun this := ⋯; Nat.maxPowDiv.go (k + 1) p (n / p) else k

theorem Nat.maxPowDiv.go_eq {k : ℕ} {p : ℕ} {n : ℕ} : Nat.maxPowDiv.go k p n = if 1 < p ∧ 0 < n ∧ n % p = 0 then Nat.maxPowDiv.go (k + 1) p (n / p) else k

theorem Nat.maxPowDiv.go_succ {k : ℕ} {p : ℕ} {n : ℕ} : Nat.maxPowDiv.go (k + 1) p n = Nat.maxPowDiv.go k p n + 1

@[simp]

theorem Nat.maxPowDiv.zero_base {n : ℕ} : Nat.maxPowDiv 0 n = 0

@[simp]

theorem Nat.maxPowDiv.zero {p : ℕ} : p.maxPowDiv 0 = 0

theorem Nat.maxPowDiv.base_mul_eq_succ {p : ℕ} {n : ℕ} (hp : 1 < p) (hn : 0 < n) : p.maxPowDiv (p * n) = p.maxPowDiv n + 1

theorem Nat.maxPowDiv.base_pow_mul {p : ℕ} {n : ℕ} {exp : ℕ} (hp : 1 < p) (hn : 0 < n) : p.maxPowDiv (p ^ exp * n) = p.maxPowDiv n + exp

theorem Nat.maxPowDiv.pow_dvd (p : ℕ) (n : ℕ) : p ^ p.maxPowDiv n ∣ n

theorem Nat.maxPowDiv.le_of_dvd {p : ℕ} {n : ℕ} {pow : ℕ} (hp : 1 < p) (hn : 0 < n) (h : p ^ pow ∣ n) : pow ≤ p.maxPowDiv n