le_mul_of_le_left

Mathlib.Algebra.Order.Monoid.Canonical.Defs

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

English

If a ≤ b, then a ≤ b·c for any c in a canonically ordered multiplicative structure.

Русский

Если а ≤ b, то а ≤ b·c для любого c.

LaTeX

$$$a \le b \rightarrow a \le b\cdot c$$$

Lean4

@[to_additive]
theorem le_mul_of_le_left : a ≤ b → a ≤ b * c :=
  le_self_mul.trans'

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

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

Разделы

Аффилиация

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