self_le_mul_right

Mathlib.Algebra.Order.Monoid.Canonical.Defs

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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