mulLeftReflectLT_of_mulLeftStrictMono

Mathlib.Algebra.Order.Monoid.Unbundled.Defs

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

English

In a group with LE and MulLeftMono, MulLeftReflectLE N holds; i.e., left translation reflects the order.

Русский

В группе с отношением порядка и левой монотонностью умножения выполняется MulLeftReflectLE.

LaTeX

$$Group N ⟹ MulLeftReflectLE N$$

Lean4

@[to_additive]
theorem mulLeftReflectLT_of_mulLeftStrictMono [Group N] [LT N] [MulLeftStrictMono N] : MulLeftReflectLT N :=
  inferInstance

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

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

Разделы

Аффилиация

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