inv_lt_one_of_one_lt

Mathlib.Algebra.Order.Group.Defs

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

English

If 1 < a, then a⁻¹ < 1.

Русский

Если 1 < a, то a⁻¹ < 1.

LaTeX

$$1 < a \Rightarrow a^{-1} < 1$$

Lean4

@[to_additive]
theorem inv_lt_one_of_one_lt : 1 < a → a⁻¹ < 1 :=
  inv_lt_one_iff_one_lt.mpr

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

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

Разделы

Аффилиация

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