mulRightReflectLT_of_mulLeftReflectLT

English

Analogous reflection result for LT: right multiplication reflects LT given left reflect LT.

Русский

Аналогично для LT: правое умножение отражает LT при условии левого отражения LT.

LaTeX

$$$\text{RightReflectLT}$ follows from $\text{LeftReflectLT}$ in a semigroup.$$

Lean4

@[to_additive]
theorem mulRightReflectLT_of_mulLeftReflectLT [CommSemigroup N] [LT N] [MulLeftReflectLT N] : MulRightReflectLT N :=
  inferInstance

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