inv_mul_le_iff_le_mul'

Mathlib.Algebra.Order.Group.Unbundled.Basic

URI: https://scilib.ai/kg/mathlib#inv_mul_le_iff_le_mul'

English

In a commutative group with a linear order, for all a,b,c, c^{-1} a ≤ b is equivalent to a ≤ b c.

Русский

В коммутативной группе с линейным порядком для всех a,b,c верно: c^{-1} a ≤ b эквивалентно a ≤ b c.

LaTeX

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

Lean4

@[to_additive]
theorem inv_mul_le_iff_le_mul' : c⁻¹ * a ≤ b ↔ a ≤ b * c := by rw [inv_mul_le_iff_le_mul, mul_comm]

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

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

Разделы

Аффилиация

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