mathlib
60fa54e7 - chore(number_theory/padics/padic_val): golf (#17885)

Commit
3 years ago
chore(number_theory/padics/padic_val): golf (#17885) Also add `padic_val_nat_dvd_iff_le` and assume `≠ 0` instead of `0 <` in `pow_succ_padic_val_nat_not_dvd`.
Author
Parents
Loading