norm_pow_natAbs — Mathlib

English

For any a ∈ E and integer n, ‖a^{n.natAbs}‖ = ‖a^n‖, i.e., norm of the positive power equals norm of the signed power.

Русский

Для любого a ∈ E и целого n выполняется ‖a^{n.natAbs}‖ = ‖a^n‖, то есть норма положительной степени совпадает с нормой знаменательно-целой степени.

LaTeX

$$$‖a^{|n|}‖ = ‖a^n‖$$$

Lean4

@[to_additive (attr := simp) norm_natAbs_smul]
theorem norm_pow_natAbs (a : E) (n : ℤ) : ‖a ^ n.natAbs‖ = ‖a ^ n‖ := by
  rw [← zpow_natCast, ← Int.abs_eq_natAbs, norm_zpow_abs]

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