Commit 2022-12-06 02:09 d5a4ef2a

View on Github →

feat: port Algebra.Divisibility.Units (#848) Mathlib SHA: e574b1a4e891376b0ef974b926da39e05da12a06

Estimated changes

added theorem IsUnit.dvd
added theorem IsUnit.dvd_mul_left
added theorem IsUnit.dvd_mul_right
added theorem IsUnit.mul_left_dvd
added theorem IsUnit.mul_right_dvd
added theorem Units.coe_dvd
added theorem Units.dvd_mul_left
added theorem Units.dvd_mul_right
added theorem Units.mul_left_dvd
added theorem Units.mul_right_dvd
added theorem isUnit_iff_dvd_one
added theorem isUnit_iff_forall_dvd
added theorem isUnit_of_dvd_one
added theorem isUnit_of_dvd_unit