Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-11 09:55 b1aef433

View on Github →

chore(algebra/ring/basic): move results on dvd (#16864) Move some results in algebra.ring.basic about dvd to algebra.ring.divisibility.

Estimated changes

deleted theorem dvd_add
deleted theorem dvd_add_iff_left
deleted theorem dvd_add_iff_right
deleted theorem dvd_add_left
deleted theorem dvd_add_right
deleted theorem dvd_add_self_left
deleted theorem dvd_add_self_right
deleted theorem dvd_iff_dvd_of_dvd_sub
deleted theorem dvd_mul_sub_mul
deleted theorem dvd_neg
deleted theorem dvd_neg_of_dvd
deleted theorem dvd_of_dvd_neg
deleted theorem dvd_of_neg_dvd
deleted theorem dvd_sub
deleted theorem has_dvd.dvd.linear_comb
deleted theorem neg_dvd
deleted theorem neg_dvd_of_dvd
deleted theorem two_dvd_bit0
deleted theorem two_dvd_bit1
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