toRightCancelSemigroup — Mathlib

English

If a semigroup with a partial order has a right-reflective right multiplication, then it forms a RightCancelSemigroup.

Русский

Если у полугруппы с частичным порядком правая операция умножения отражает порядок, то она образует правую отменяемую полугруппу.

LaTeX

$$$MulRightReflectLE \\\\alpha \\\\Rightarrow RightCancelSemigroup \\\\alpha$$$

Lean4

/-- A semigroup with a partial order and satisfying `RightCancelSemigroup`
(i.e. `a * c < b * c → a < b`) is a `RightCancelSemigroup`. -/
@[to_additive /-- An additive semigroup with a partial order and satisfying `AddRightCancelSemigroup`
    (`a + c < b + c → a < b`) is a `AddRightCancelSemigroup`. -/
    ]
def toRightCancelSemigroup [MulRightReflectLE α] : RightCancelSemigroup α :=
  { ‹Semigroup α› with mul_right_cancel := fun _ _ _ => mul_right_cancel'' }

Похожие утверждения