self_le_mul_left

Mathlib.Algebra.Order.Monoid.Canonical.Defs

URI: https://scilib.ai/kg/mathlib#self_le_mul_left

English

Similarly, a ≤ b·a holds for all a,b in a canonically ordered multiplicative structure.

Русский

Аналогично, для любых a,b в канонически упорядоченном моноиде выполняется a ≤ b·a.

LaTeX

$$$a \le b\cdot a$$$

Lean4

@[to_additive (attr := simp)]
theorem self_le_mul_left (a b : α) : a ≤ b * a :=
  le_mul_self

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

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

Разделы

Аффилиация

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