Commit 2025-04-03 14:46 b7e7d34b

View on Github →

feat: mixin ordered algebraic typeclasses (#20593)

Estimated changes

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

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

added theorem IsOrderedCancelMonoid.toMulRightReflectLT

deleted theorem OrderedCancelCommMonoid.toMulRightReflectLT

deleted theorem OrderedCommMonoid.toMulRightMono

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

added theorem IsOrderedRing.of_mul_nonneg

added theorem IsOrderedRing.toIsStrictOrderedRing

added theorem IsStrictOrderedRing.of_mul_pos

Modified Mathlib/Data/Real/Basic.lean

Modified Mathlib/Order/Interval/Finset/Box.lean