# Documentation

Mathlib.Data.Nat.MaxPowDiv

# 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

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_eq {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 = + 1
@[simp]
theorem Nat.maxPowDiv.zero_base {n : } :
= 0
@[simp]
theorem Nat.maxPowDiv.zero {p : } :
= 0
theorem Nat.maxPowDiv.base_mul_eq_succ {p : } {n : } (hp : 1 < p) (hn : 0 < n) :
Nat.maxPowDiv p (p * n) = + 1
theorem Nat.maxPowDiv.base_pow_mul {p : } {n : } {exp : } (hp : 1 < p) (hn : 0 < n) :
Nat.maxPowDiv p (p ^ exp * n) = + exp
theorem Nat.maxPowDiv.pow_dvd (p : ) (n : ) :
p ^ n
theorem Nat.maxPowDiv.le_of_dvd {p : } {n : } {pow : } (hp : 1 < p) (hn : 0 < n) (h : p ^ pow n) :
pow