mul_inv_le_mul_inv_iff'

Mathlib.Algebra.Order.Group.Unbundled.Basic

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

← MathLib Explorer

English

In a commutative group with order, a*b^{-1} ≤ d^{-1} c is equivalent to a d ≤ c b.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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