mabs_pow — Mathlib

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)]

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