mulLeftStrictMono_of_mulLeftMono — Mathlib

English

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

Русский

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

LaTeX

$$$\text{LeftStrictMono}$ holds under $\text{LeftCancel}$ and order-theoretic assumptions.$$

Lean4

@[to_additive]
instance mulLeftStrictMono_of_mulLeftMono [Mul N] [IsLeftCancelMul N] [PartialOrder N] [MulLeftMono N] :
    MulLeftStrictMono N where elim a _ _ bc := (CovariantClass.elim a bc.le).lt_of_ne ((mul_ne_mul_right a).mpr bc.ne)

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