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

Equations
Instances For
    @[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

    Equations
    Instances For
      theorem Nat.maxPowDiv.go_succ {k : } {p : } {n : } :
      @[simp]
      @[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 : 0 < n) (h : p ^ pow n) :
      pow p.maxPowDiv n