Commit 2022-12-10 16:28 60fa54e7

View on Github →

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.

Estimated changes

Modified src/number_theory/padics/padic_val.lean

added theorem padic_val_nat_dvd_iff_le

modified theorem pow_succ_padic_val_nat_not_dvd

Modified src/ring_theory/polynomial/cyclotomic/eval.lean