le_inv_self_iff

Mathlib.Algebra.Order.Group.Defs

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

English

The lemma inv_lt_self_iff: a⁻¹ < a iff 1 < a holds in an ordered group.

Русский

Лемма inv_lt_self_iff: a⁻¹ < a эквивалентно 1 < a в упорядоченной группе.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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