mathlib3

e48c2af4 - feat(data/padics/padic_norm): New padic_val_nat convenience functions (#2970)

feat(data/padics/padic_norm): New padic_val_nat convenience functions (#2970) Convenience functions to allow us to deal either with the p-adic valuation or with multiplicity in the naturals, depending on what is locally convenient.