mathlib3

53541ffc - refactor(number_theory/padics/padic_val): make prime implicit (#15221)

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.