mathlib3
e8638a0f - feat(algebra/divisibility/basic): Dot notation aliases (#18698)

Commit
2 years ago
feat(algebra/divisibility/basic): Dot notation aliases (#18698) A few convenience shortcuts for `dvd` along with some simple `nat` lemmas. Also * Drop `neg_dvd_of_dvd`/`dvd_of_neg_dvd`/`dvd_neg_of_dvd`/`dvd_of_dvd_neg` in favor of the aforementioned shortcuts. * Remove explicit arguments to `dvd_neg`/`neg_dvd`. * Drop `int.of_nat_dvd_of_dvd_nat_abs`/`int.dvd_nat_abs_of_of_nat_dvd` because they are the two directions of `int.coe_nat_dvd_left`. * Move `group_with_zero.to_cancel_monoid_with_zero` from `algebra.group_with_zero.units.basic` back to `algebra.group_with_zero.basic`. It was erroneously moved during the Great Splits.
Author
Parents
Loading