English
For any a in G, either |a|_m = a and a ≥ 1, or |a|_m = a^{-1} and a < 1.
Русский
Для любого a: либо |a|ₘ = a и a ≥ 1, либо |a|ₘ = a^{-1} и a < 1.
LaTeX
$$\left( |a|_m = a \land 1 \le a \right) \lor \left( |a|_m = a^{-1} \land a < 1 \right)$$
Lean4
/-- For an element `a` of a multiplicative linear ordered group,
either `|a|ₘ = a` and `1 ≤ a`, or `|a|ₘ = a⁻¹` and `a < 1`. -/
@[to_additive /-- For an element `a` of an additive linear ordered group,
either `|a| = a` and `0 ≤ a`, or `|a| = -a` and `a < 0`.
Use cases on this lemma to automate linarith in inequalities -/
]
theorem mabs_cases (a : G) : |a|ₘ = a ∧ 1 ≤ a ∨ |a|ₘ = a⁻¹ ∧ a < 1 := by cases le_or_gt 1 a <;> simp [*, le_of_lt]
