Commit 2022-06-09 13:27 c0b3ed79
View on Github →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.