Commit 2026-04-24 17:35 d480e9ea

View on Github →

refactor(Algebra/Order/Monoid/Unbundled/Defs): upgrade *ReflectLE from abbrevs to classes (#37393) ... to mitigate performance regression caused by #36629. Currently the 4 classes {Mul/Add}{Left/Right}ReflectLE are an abbrev for ContravariantClass so when TC-search tries to synthesize them it ends up looking through all the ContravariantClass instances and not just the relevant ones.

Estimated changes

Modified Mathlib/Algebra/Order/Group/Multiset.lean

Modified Mathlib/Algebra/Order/GroupWithZero/Unbundled/Defs.lean

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

modified theorem IsOrderedCancelMonoid.toMulRightReflectLT

Modified Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean

modified theorem le_of_mul_le_mul_left'

modified theorem le_of_mul_le_mul_right'

modified theorem mul_le_mul_iff_left

modified theorem mul_le_mul_iff_right

Modified Mathlib/Algebra/Order/Monoid/Unbundled/Defs.lean

deleted theorem Group.mulLeftReflectLE_of_mulLeftMono

deleted theorem Group.mulRightReflectLE_of_mulRightMono

modified theorem Group.mulRightReflectLT_of_mulRightStrictMono

deleted theorem mulLeftStrictMono_of_mulLeftReflectLE

deleted theorem mulRightReflectLE_of_mulLeftReflectLE

deleted theorem mulRightStrictMono_of_mulRightReflectLE

added theorem rel_iff_cov'

Modified Mathlib/Algebra/Order/Monoid/Unbundled/OrderDual.lean

Modified Mathlib/Algebra/Order/Positive/Ring.lean

Modified Mathlib/Data/DFinsupp/Order.lean

Modified Mathlib/Data/Finsupp/Order.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean