mulRightReflectLE_of_mulLeftReflectLE

English

From left-reflective LE, derive right-reflective LE in a commutative semigroup.

Русский

Из левого отражающего LE вывожу правое отражающее LE в коммутативной полугруппе.

LaTeX

$$$\text{RightReflectLE}$ follows from $\text{LeftReflectLE}$ in a commutative semigroup.$$

Lean4

@[to_additive]
theorem mulRightReflectLE_of_mulLeftReflectLE [CommSemigroup N] [LE N] [MulLeftReflectLE N] : MulRightReflectLE N :=
  inferInstance

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