mul_le_mul_right

Mathlib.Algebra.Order.Monoid.Unbundled.Units

URI: https://scilib.ai/kg/mathlib#IsUnit.mul_le_mul_right

English

Let a be IsUnit in a monoid with order; then b · a ≤ c · a iff b ≤ c.

Русский

Пусть a является IsUnit в моноиде с порядком; тогда b·a ≤ c·a эквивалентно b ≤ c.

LaTeX

$$$b \cdot a \le c \cdot a \iff b \le c$$$

Lean4

theorem mul_le_mul_right : a * c ≤ b * c ↔ a ≤ b :=
  hc.unit.mul_le_mul_iff_right

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

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

Разделы

Аффилиация

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