Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-29 04:21 9a1c0a6e

View on Github →

feat(data/padics/padic_norm) Fix namespacing of padic_val_nat (#3207) No longer need we padic_val_rat.padic_val_nat.

Estimated changes

added def padic_val_nat
added theorem padic_val_nat_def
added theorem padic_val_rat_of_nat