Commit 2022-03-01 23:58 4ba9098e

View on Github →

feat(algebra/euclidean_domain,data/int/basic): dvd_div_of_mul_dvd (#12382) We have a separate int and euclidean_domain version as euclidean_domain isn't pulled in by int.basic.

Estimated changes

Modified src/algebra/euclidean_domain.lean

added theorem euclidean_domain.dvd_div_of_mul_dvd

Modified src/data/int/basic.lean

added theorem int.div_dvd_of_dvd

deleted theorem int.div_dvd_of_ne_zero_dvd

added theorem int.dvd_div_of_mul_dvd