lt_inv_self_iff

Mathlib.Algebra.Order.Group.Defs

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

English

In a linearly ordered group, a < a⁻¹ if and only if a < 1 (alternative simplification).

Русский

В линейно упорядоченной группе: a < a⁻¹ эквивалентно a < 1 (упрощенная версия).

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem lt_inv_self_iff : a < a⁻¹ ↔ a < 1 := by simp [← not_iff_not]

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

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

Разделы

Аффилиация

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