le_inv_mul_iff_le

Mathlib.Algebra.Order.Group.Unbundled.Basic

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

English

In a group with order and left-mono, 1 ≤ b⁻¹ a if and only if b ≤ a.

Русский

В группе с порядком и левым монотонным умножением: 1 ≤ b⁻¹ a тогда и только тогда, когда b ≤ a.

LaTeX

$$$1 \le b^{-1} a \iff b \le a$$$

Lean4

@[to_additive]
theorem le_inv_mul_iff_le : 1 ≤ b⁻¹ * a ↔ b ≤ a := by rw [← mul_le_mul_iff_left b, mul_one, mul_inv_cancel_left]

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

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

Разделы

Аффилиация

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