mul_inv_lt_one_iff

Mathlib.Algebra.Order.Group.Unbundled.Basic

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

English

For b a^{-1} < 1 is equivalent to b < a in a suitable ordered group.

Русский

Для b a^{-1} < 1 эквивалентно b < a в упорядоченной группе.

LaTeX

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

Lean4

@[to_additive]
theorem mul_inv_lt_one_iff : b * a⁻¹ < 1 ↔ b < a :=
  _root_.trans mul_inv_lt_iff_lt_mul <| by rw [one_mul]

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

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

Разделы

Аффилиация

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