Commit 2026-03-30 17:54 a4cbabc8

View on Github →

chore(Algebra/Order/Monoid/Unbundled/Basic): replace mul_left_cancel'' with an IsLeftCancelMul instance (#36629)

Estimated changes

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

modified def Contravariant.toLeftCancelSemigroup

modified def Contravariant.toRightCancelSemigroup

deleted theorem mul_left_cancel''

deleted theorem mul_right_cancel''