nnnorm_pow_natAbs — Mathlib

English

Let E be a seminormed group and a an element of E. For every integer n, the NN-real norm of a raised to the natural absolute value of n equals the NN-real norm of a raised to n: ‖a^{n.natAbs}‖₊ = ‖a^n‖₊.

Русский

Пусть E — полугруппа с полугипернормой, a — элемент E. Для любого целого числа n NN-норма a^{|n|} равна NN-норме a^n: ‖a^{n.natAbs}‖₊ = ‖a^n‖₊.

LaTeX

$$$$ \\|a^{\\,n.natAbs}\\|_{+} = \\|a^{\\,n}\\|_{+} $$$$

Lean4

@[to_additive (attr := simp) nnnorm_natAbs_smul]
theorem nnnorm_pow_natAbs (a : E) (n : ℤ) : ‖a ^ n.natAbs‖₊ = ‖a ^ n‖₊ :=
  NNReal.eq <| norm_pow_natAbs a n

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