English
In a linearly ordered commutative group, the magnitude of a power equals the power of the magnitude: |a^n| = |a|^n for all n ∈ ℕ.
Русский
В линейно упорядоченной коммутативной группе модуль a^n равен модулю a в степени n.
LaTeX
$$$$ |a^n| = |a|^n $$$$
Lean4
@[to_additive]
theorem mabs_pow (n : ℕ) (a : G) : |a ^ n|ₘ = |a|ₘ ^ n :=
by
obtain ha | ha := le_total a 1
· rw [mabs_of_le_one ha, ← mabs_inv, ← inv_pow, mabs_of_one_le]
exact one_le_pow_of_one_le' (one_le_inv'.2 ha) n
· rw [mabs_of_one_le ha, mabs_of_one_le (one_le_pow_of_one_le' ha n)]