Commit 2023-06-18 08:20 9ccc8b74

View on Github →

feat: add Nat.maxPowDiv (#5158) Adds tail recursive definition of maximal k such that p^k | n for p, n : Nat and csimp theorem relating it to Nat.padicValNat

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/MaxPowDiv.lean

added theorem Nat.maxPowDiv.base_mul_eq_succ

added theorem Nat.maxPowDiv.base_pow_mul

added theorem Nat.maxPowDiv.go_eq

added theorem Nat.maxPowDiv.go_succ

added theorem Nat.maxPowDiv.le_of_dvd

added theorem Nat.maxPowDiv.pow_dvd

added theorem Nat.maxPowDiv.zero

added theorem Nat.maxPowDiv.zero_base

added def Nat.maxPowDiv

Modified Mathlib/NumberTheory/Padics/PadicVal.lean

added theorem padicValNat.maxPowDiv_eq_multiplicity

added theorem padicValNat.maxPowDiv_eq_multiplicity_get

added theorem padicValNat.padicValNat_eq_maxPowDiv

Created test/MaxPowDiv.lean