mulRightStrictMono_of_mulRightMono

English

In a semigroup with right-cancellation, right multiplication is strictly monotone.

Русский

В полугруппе с правой отменяемостью правая операция умножения строго монотонна.

LaTeX

$$$\text{RightStrictMono}$ holds under $\text{RightCancel}$ and order-structure assumptions.$$

Lean4

@[to_additive]
instance mulRightStrictMono_of_mulRightMono [Mul N] [IsRightCancelMul N] [PartialOrder N] [MulRightMono N] :
    MulRightStrictMono N where elim a _ _ bc := (CovariantClass.elim a bc.le).lt_of_ne ((mul_ne_mul_left a).mpr bc.ne)

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