English
If a semigroup with a partial order has a left-reflective left multiplication, then it forms a LeftCancelSemigroup.
Русский
Если у полугруппы с частичным порядком левая операция умножения отражает порядок, то она образует левую отменяемую полугруппу.
LaTeX
$$$MulLeftReflectLE \\\\alpha \\\\Rightarrow LeftCancelSemigroup \\\\alpha$$$
Lean4
/-- A semigroup with a partial order and satisfying `LeftCancelSemigroup`
(i.e. `a * c < b * c → a < b`) is a `LeftCancelSemigroup`. -/
@[to_additive /-- An additive semigroup with a partial order and satisfying `AddLeftCancelSemigroup`
(i.e. `c + a < c + b → a < b`) is a `AddLeftCancelSemigroup`. -/
]
def toLeftCancelSemigroup [MulLeftReflectLE α] : LeftCancelSemigroup α :=
{ ‹Semigroup α› with mul_left_cancel := fun _ _ _ => mul_left_cancel'' }
/- This is not instance, since we want to have an instance from `RightCancelSemigroup`s
to the appropriate covariant class. -/
