mabs_eq_self

Mathlib.Algebra.Order.Group.Abs

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

English

For any a in G, |a|_m = a if and only if a ≥ 1.

Русский

Для любого a: |a|ₘ = a тогда и только тогда, когда a ≥ 1.

LaTeX

$$|a|_m = a \iff 1 \le a$$

Lean4

@[to_additive (attr := simp)]
theorem mabs_eq_self : |a|ₘ = a ↔ 1 ≤ a := by rw [mabs_eq_max_inv, max_eq_left_iff, inv_le_self_iff]

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

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

Разделы

Аффилиация

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