norm_pow

Mathlib.Analysis.Complex.Norm

URI: https://scilib.ai/kg/mathlib#Complex.norm_pow

English

For any z ∈ ℂ and natural n, the norm of the n-th power equals the n-th power of the norm: ‖z^n‖ = ‖z‖^n.

Русский

Для любого z ∈ ℂ и натурального n выполняется ‖z^n‖ = ‖z‖^n.

LaTeX

$$$\forall z \in \mathbb{C},\; \forall n \in \mathbb{N},\; \|z^n\| = \|z\|^n$$$

Lean4

protected theorem norm_pow (z : ℂ) (n : ℕ) : ‖z ^ n‖ = ‖z‖ ^ n :=
  map_pow isAbsoluteValueNorm.abvHom _ _

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

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

Разделы

Аффилиация

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