# 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 =
Instances For
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
Instances For
theorem Nat.maxPowDiv.go_succ {k : } {p : } {n : } :
Nat.maxPowDiv.go (k + 1) p n = + 1
@[simp]
theorem Nat.maxPowDiv.zero_base {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