mathlib3
93a37647 - chore(algebra/ring/basic): drop commutativity assumptions from some division lemmas (#8334)

Commit
4 years ago
chore(algebra/ring/basic): drop commutativity assumptions from some division lemmas (#8334) * Removes `dvd_neg_iff_dvd`, `neg_dvd_iff_dvd` which duplicated `dvd_neg`, `neg_dvd`. * Generalizes `two_dvd_bit0` to non-commutative semirings. * Generalizes a bunch of lemmas from `comm_ring` to `ring`. * Adds `even_neg` for `ring` to replace `int.even_neg`.
Parents
Loading