Commit 2022-05-04 15:53 0038a043

View on Github →

feat(data/int/cast): int cast division lemmas (#13929) Adds lemmas for passing int cast through division, and renames the nat versions from nat.cast_dvd to nat.cast_div. Also some golf.

Estimated changes

Modified src/algebra/char_zero.lean

added theorem nat.cast_div_char_zero

deleted theorem nat.cast_dvd_char_zero

Modified src/data/int/cast.lean

added theorem int.cast_div

Modified src/data/int/char_zero.lean

added theorem int.cast_div_char_zero

Modified src/data/nat/cast.lean

added theorem nat.cast_div

deleted theorem nat.cast_dvd

Modified src/data/nat/totient.lean

Modified src/number_theory/bernoulli.lean

Modified src/number_theory/von_mangoldt.lean

Modified src/ring_theory/discriminant.lean

Modified src/ring_theory/power_series/well_known.lean