Commit 2024-12-21 08:00 1c080cc4

View on Github →

refactor: make PadicInt.valuation ℕ-valued (#19858) It is currently ℤ-valued, but always nonnegative. Also rename the misnamed norm_eq_pow_val to norm_eq_zpow_neg_valuation From FLT Closes https://github.com/ImperialCollegeLondon/FLT/issues/277

Estimated changes

modified theorem PadicInt.coe_eq_zero
modified theorem PadicInt.coe_ne_zero
deleted theorem PadicInt.norm_eq_pow_val
modified def PadicInt.valuation
added theorem PadicInt.valuation_coe
added theorem PadicInt.valuation_mul
deleted theorem PadicInt.valuation_nonneg
modified theorem PadicInt.valuation_one
modified theorem PadicInt.valuation_p
added theorem PadicInt.valuation_pow
modified theorem PadicInt.valuation_zero
modified def PadicInt
added theorem Padic.le_valuation_add
deleted theorem Padic.norm_eq_pow_val
added theorem Padic.valuation_inv
deleted theorem Padic.valuation_map_add
deleted theorem Padic.valuation_map_mul
added theorem Padic.valuation_mul
added theorem Padic.valuation_pow
added theorem Padic.valuation_zpow
deleted theorem PadicSeq.norm_eq_pow_val