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

@[irreducible]

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

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

@[simp]

theorem Nat.maxPowDiv.zero_base {n : ℕ} : 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

@[irreducible]

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 : n ≠ 0) (h : p ^ pow ∣ n) : pow ≤ p.maxPowDiv n