Commit 2022-12-06 13:47 fde5a99f

View on Github →

feat: port Algebra.GroupWithZero.Divisibility (#870) mathlib3 SHA: f1a2caaf51ef593799107fe9a8d5e411599f3996

Estimated changes

added def DvdNotUnit
added theorem dvd_and_not_dvd_iff
added theorem dvd_zero
added theorem eq_zero_of_zero_dvd
added theorem mul_dvd_mul_iff_left
added theorem mul_dvd_mul_iff_right
added theorem ne_zero_of_dvd_ne_zero
added theorem zero_dvd_iff