mulRightMono_of_mulLeftMono — Mathlib

English

In a commutative semigroup with LE, if left monotonicity holds, then right multiplication is monotone.

Русский

В коммутативной полугруппе с LE, при условии монотонности слева, правая умножение монотонна.

LaTeX

$$$\text{RightMono}$ holds from $\text{LeftMono}$ in a commutative semigroup with LE.$$

Lean4

@[to_additive]
theorem mulRightMono_of_mulLeftMono [CommSemigroup N] [LE N] [MulLeftMono N] : MulRightMono N :=
  inferInstance

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