mulRightReflectLE_of_mulRightMono

Mathlib.Algebra.Order.Monoid.Unbundled.Defs

URI: https://scilib.ai/kg/mathlib#Group.mulRightReflectLE_of_mulRightMono

English

In a group N with LE and MulRightMono, MulRightReflectLE N holds; left translation on the right reflects the order.

Русский

В группе N с LE и правым монотонным умножением выполняется MulRightReflectLE.

LaTeX

$$Group N ⟹ MulRightReflectLE N$$

Lean4

@[to_additive]
theorem mulRightReflectLE_of_mulRightMono [Group N] [LE N] [MulRightMono N] : MulRightReflectLE N :=
  inferInstance

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru