le_self_mul

Mathlib.Algebra.Order.Monoid.Canonical.Defs

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

English

In a canonically ordered multiplicative structure, for any a,b, a ≤ a·b.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem le_self_mul : a ≤ a * b :=
  CanonicallyOrderedMul.le_self_mul _ _

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

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

Разделы

Аффилиация

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