mathlib

c0b3ed79 - feat(number_theory/padics/padic_val): add `padic_val_nat_def'` and generalise `pow_padic_val_nat_dvd` (#14637)

feat(number_theory/padics/padic_val): add `padic_val_nat_def'` and generalise `pow_padic_val_nat_dvd` (#14637) add `padic_val_nat_def' (hn : 0 < n) (hp : p ≠ 1) : ↑(padic_val_nat p n) = multiplicity p n` `pow_padic_val_nat_dvd : p ^ (padic_val_nat p n) ∣ n` holds without the assumption that `p` is prime.