Commit 2022-12-06 17:05 6a007d38

View on Github →

feat: port Algebra.Ring.Divisibility (#864) Based off mathlib3 SHA: f1a2caaf51ef593799107fe9a8d5e411599f3996

Estimated changes

added theorem Dvd.dvd.linear_comb
added theorem dvd_add
added theorem dvd_add_iff_left
added theorem dvd_add_iff_right
added theorem dvd_add_left
added theorem dvd_add_right
added theorem dvd_add_self_left
added theorem dvd_add_self_right
added theorem dvd_iff_dvd_of_dvd_sub
added theorem dvd_mul_sub_mul
added theorem dvd_neg
added theorem dvd_neg_of_dvd
added theorem dvd_of_dvd_neg
added theorem dvd_of_neg_dvd
added theorem dvd_sub
added theorem neg_dvd
added theorem neg_dvd_of_dvd
added theorem two_dvd_bit0
added theorem two_dvd_bit1