Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-16 13:03 894c8c22

View on Github →

refactor(number_theory/padics/padic_val): make prime implicit (#15221) Make the variable denoting the prime in theorems related to padic_val_nat, padic_val_int, padic_val_rat, and padic_norm implicit, since they seem to be redundant and inferable in all use cases, but the variable in their definitions remain explicit.

Estimated changes

modified theorem padic_norm.dvd_iff_norm_le
modified theorem padic_norm.of_nat
modified theorem padic_norm.padic_norm_p
modified theorem padic_norm.sum_le'
modified theorem padic_norm.sum_lt'
modified theorem dvd_of_one_le_padic_val_nat
modified theorem one_le_padic_val_nat_of_dvd
modified theorem padic_val_int.mul
modified theorem padic_val_int_dvd
modified theorem padic_val_int_dvd_iff
modified theorem padic_val_int_mul_eq_succ
modified theorem padic_val_int_self
modified theorem padic_val_nat_def'
modified theorem padic_val_nat_def
modified theorem padic_val_nat_dvd_iff
modified theorem padic_val_nat_primes
modified theorem padic_val_nat_self
modified theorem padic_val_rat.of_int
modified theorem padic_val_rat.of_nat
modified theorem padic_val_rat_of_nat