mul_inv_lt_mul_inv_iff' — Mathlib

English

For elements a,b,c,d in a commutative group with order and left-strict mono, a*b^{-1} < c*d^{-1} iff a*d < c*b.

Русский

Для элементов a,b,c,d в коммутативной группе с порядком и лево-монотоничностью, a*b^{-1} < c*d^{-1} эквивалентно a*d < c*b.

LaTeX

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

Lean4

@[to_additive add_neg_lt_add_neg_iff]
theorem mul_inv_lt_mul_inv_iff' : a * b⁻¹ < c * d⁻¹ ↔ a * d < c * b := by
  rw [mul_comm c, mul_inv_lt_inv_mul_iff, mul_comm]

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