nnnorm_zpow_abs

Mathlib.Analysis.Normed.Group.Basic

URI: https://scilib.ai/kg/mathlib#nnnorm_zpow_abs

English

The NNReal norm of the absolute value of a power equals the NNReal norm of the same integer power.

Русский

NNReal-норма модуля степени равна NNReal-норме той же степени.

LaTeX

$$$\\|a^{|n|}\\|_+ = \\|a^{n}\\|_+$$$

Lean4

@[to_additive (attr := simp) nnnorm_abs_zsmul]
theorem nnnorm_zpow_abs (a : E) (n : ℤ) : ‖a ^ |n|‖₊ = ‖a ^ n‖₊ :=
  NNReal.eq <| norm_zpow_abs a n

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru