mabs_eq_inv_self

Mathlib.Algebra.Order.Group.Abs

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

English

For any a in G, |a|_m = a^{-1} if and only if a ≤ 1.

Русский

Для любого a: |a|ₘ = a^{-1} тогда и только тогда, когда a ≤ 1.

LaTeX

$$|a|_m = a^{-1} \iff a \le 1$$

Lean4

@[to_additive (attr := simp)]
theorem mabs_eq_inv_self : |a|ₘ = a⁻¹ ↔ a ≤ 1 := by rw [mabs_eq_max_inv, max_eq_right_iff, le_inv_self_iff]

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

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

Разделы

Аффилиация

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