Commit 2026-03-13 10:21 4da16c39

View on Github →

feat: add generalizations of some padicVal{Nat,Int} lemmas (#34588) Also drop the unnecessary primality condition from padicValInt_dvd. From flt-regular.

Estimated changes

Modified Mathlib/NumberTheory/Padics/PadicVal/Basic.lean

modified theorem padicValInt.mul

modified theorem padicValInt_dvd_iff

added theorem padicValInt_dvd_iff_of_ne_one

modified theorem padicValInt_mul_eq_succ

modified theorem padicValInt_self

added theorem padicValNat_dvd_iff_le_of_ne_one

added theorem padicValNat_dvd_iff_of_ne_one

Modified Mathlib/NumberTheory/Padics/PadicVal/Defs.lean

added theorem padicValNat_eq_emultiplicity_of_ne_one