Commit 2026-10-28 10:44 e2bb1c90

View on Github →

chore(Algebra/Order): split out the order on Associates (#45247) ... and split into the Monoid and MonoidWithZero parts. This is so that I can import Associates in Algebra.GroupWithZero.WithZero without triggering the assert_not_exists IsOrderedMonoid.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/BigOperators/Associated.lean

Modified Mathlib/Algebra/GCDMonoid/Basic.lean

Modified Mathlib/Algebra/GroupWithZero/Associated.lean

deleted theorem Associates.Prime.le_or_le

deleted theorem Associates.dvdNotUnit_iff_lt

deleted theorem Associates.dvdNotUnit_of_lt

deleted theorem Associates.dvd_eq_le

deleted theorem Associates.dvd_of_mk_le_mk

deleted theorem Associates.isUnit_iff_eq_bot

deleted theorem Associates.le_mul_left

deleted theorem Associates.le_mul_right

deleted theorem Associates.le_of_mul_le_mul_left

deleted theorem Associates.le_one_iff

deleted theorem Associates.mk_le_mk_iff_dvd

deleted theorem Associates.mk_le_mk_of_dvd

deleted theorem Associates.mul_mono

deleted theorem Associates.one_or_eq_of_le_of_prime

Created Mathlib/Algebra/Order/GroupWithZero/Associated.lean

added theorem Associates.Prime.le_or_le

added theorem Associates.dvdNotUnit_iff_lt

added theorem Associates.dvdNotUnit_of_lt

added theorem Associates.le_of_mul_le_mul_left

added theorem Associates.le_one_iff

added theorem Associates.one_or_eq_of_le_of_prime

Modified Mathlib/Algebra/Order/Monoid/Associated.lean

added theorem Associates.dvd_eq_le

added theorem Associates.dvd_of_mk_le_mk

added theorem Associates.isUnit_iff_eq_bot

added theorem Associates.le_mul_left

added theorem Associates.le_mul_right

added theorem Associates.mk_le_mk_iff_dvd

added theorem Associates.mk_le_mk_of_dvd

added theorem Associates.mul_mono