mathlib3
710a76e7 - chore(algebra/divisibility): help dot notation on `dvd` (#8766)

Commit
4 years ago
chore(algebra/divisibility): help dot notation on `dvd` (#8766) Add aliases * `dvd_mul_of_dvd_left` -> `has_dvd.dvd.mul_right` * `dvd_mul_of_dvd_right` -> `has_dvd.dvd.mul_left` Add, to help with a few proofs, * `dvd_rfl` * `dvd_pow_self` Use `has_dvd.dvd.trans` more largely.
Author
Parents
Loading