norm_zpow

Mathlib.Analysis.Complex.Norm

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

English

For any z ∈ ℂ and integer n, the norm of z^n 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{Z},\; \|z^n\| = \|z\|^n$$$

Lean4

protected theorem norm_zpow (z : ℂ) (n : ℤ) : ‖z ^ n‖ = ‖z‖ ^ n :=
  map_zpow₀ isAbsoluteValueNorm.abvHom _ _

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

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

Разделы

Аффилиация

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