Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-21 12:09 82615017

View on Github →

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.

Estimated changes

modified theorem dvd_of_one_le_padic_val_nat
added theorem padic_val_int.mul
added theorem padic_val_int.of_nat
added theorem padic_val_int.self
added def padic_val_int
added theorem padic_val_int_dvd
added theorem padic_val_int_dvd_iff
added theorem padic_val_int_self
added theorem padic_val_nat.self
modified theorem padic_val_nat_def
added theorem padic_val_nat_dvd_iff
deleted theorem padic_val_nat_of_not_dvd
deleted theorem padic_val_nat_one
deleted theorem padic_val_nat_zero
added theorem padic_val_rat.of_int
added theorem padic_val_rat.of_nat
added theorem padic_val_rat.self
deleted theorem padic_val_rat_def
modified theorem padic_val_rat_of_nat