nnnorm_zpow_isUnit — Mathlib

English

For any element a in a seminormed group E and any integer n that is a unit in Z, the NN-norm of a^n equals the NN-norm of a: ‖a^n‖₊ = ‖a‖₊.

Русский

Пусть a ∈ E и n ∈ ℤ является единицей в ℤ. Тогда NN-норма a^n равна NN-норме a: ‖a^n‖₊ = ‖a‖₊.

LaTeX

$$$$ \\|a^{\\,n}\\|_{+} = \\|a\\|_{+} \\quad\\text{при } n\\text{ unit in } \\mathbb Z $$$$

Lean4

@[to_additive nnnorm_isUnit_zsmul]
theorem nnnorm_zpow_isUnit (a : E) {n : ℤ} (hn : IsUnit n) : ‖a ^ n‖₊ = ‖a‖₊ :=
  NNReal.eq <| norm_zpow_isUnit a hn

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