mathlib

mathlib copied to clipboard

There are still probably things that can be done to improve the number_theory/padic_norm.lean. Some ideas:

• [x] Split the file in two at the definition padic_norm with that latter part being called padic_norm.lean and the first part being padic_val.lean. See #13576
• [ ] There are a lot of lemmas with [prime p] typeclass argument which are actually only need something like p \ne 1. Perhaps some of these are useful, but they could be named more consistently.
• [ ] Perhaps we could do a better job of ordering lemmas, I think there are several padic_val_nat sections.
• [ ] As I think Michael Stoll suggested, it may be better to put the definition of padic_val_int before padic_val_nat.

Originally posted by @BoltonBailey in https://github.com/leanprover-community/mathlib/issues/12454#issuecomment-1099161892