Mathlib Changelog
v4
Changelog
About
Github
Theorem
PadicInt.norm_eq_zpow_neg_valuation
Modification history
2024-12-21 08:00
Mathlib/NumberTheory/Padics/PadicIntegers.lean
refactor: make `PadicInt.valuation` `ℕ`-valued (#19858) …
Added
PadicInt.norm_eq_zpow_neg_valuation
View on Github →