Commit 2020-06-06 17:40 e48c2af4

View on Github →

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.

Estimated changes

Modified src/data/padics/padic_norm.lean

added def padic_val_rat.padic_val_nat

added theorem padic_val_rat.padic_val_nat_def

added theorem padic_val_rat.padic_val_rat_of_nat

added theorem padic_val_rat.zero_le_padic_val_rat_of_nat