Commit 2022-11-28 22:47 104cff4d

View on Github →

feat: port Algebra.Order.Monoid.Cancel.Defs (#774) sha 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/Group.lean

Deleted Mathlib/Algebra/Order/Monoid/Cancel.lean

Created Mathlib/Algebra/Order/Monoid/Cancel/Defs.lean

added theorem OrderedCancelCommMonoid.lt_of_mul_lt_mul_left