mathlib3
82615017 - refactor(number_theory/padics/padic_norm): Switch nat and rat definitions (#12454)

Commit
4 years ago
refactor(number_theory/padics/padic_norm): Switch nat and rat definitions (#12454) Switches the order in which `padic_val_nat` and `padic_val_rat` are defined. This PR has also expanded to add `padic_val_int` and some API lemmas for that.
Author
Parents
Loading