English
For any element a in a commutative group with an order, and any integer n, the magnitude of a raised to n equals the magnitude of a raised to |n|: |a^n| = |a|^{|n|}.
Русский
Для любого элемента a в коммутативной группе с порядком и любого целого числа n выполняется равенство модуля a^n и модуля a в степени |n|: |a^n| = |a|^{|n|}.
LaTeX
$$$\displaystyle |a^n| = |a|^{|n|}$$$
Lean4
@[to_additive]
theorem mabs_zpow (n : ℤ) (a : α) : |a ^ n|ₘ = |a|ₘ ^ |n| :=
by
obtain n0 | n0 := le_total 0 n
· obtain ⟨n, rfl⟩ := Int.eq_ofNat_of_zero_le n0
simp only [mabs_pow, zpow_natCast, Nat.abs_cast]
· obtain ⟨m, h⟩ := Int.eq_ofNat_of_zero_le (neg_nonneg.2 n0)
rw [← mabs_inv, ← zpow_neg, ← abs_neg, h, zpow_natCast, Nat.abs_cast, zpow_natCast]
exact mabs_pow m _
