norm_cpow_of_ne_zero — Mathlib

English

If z ≠ 0, then ∥z^w∥ = ∥z∥^{Re w} / exp(arg z · Im w).

Русский

Если z ≠ 0, то |z^w| = |z|^{Re w} / exp(Arg(z) · Im w).

LaTeX

$$$z \neq 0 \Rightarrow \|z^{w}\| = \|z\|^{\Re w} / e^{\operatorname{Arg}(z) \cdot \Im w}$$$

Lean4

theorem norm_cpow_of_ne_zero {z : ℂ} (hz : z ≠ 0) (w : ℂ) : ‖z ^ w‖ = ‖z‖ ^ w.re / Real.exp (arg z * im w) := by
  rw [cpow_def_of_ne_zero hz, norm_exp, mul_re, log_re, log_im, Real.exp_sub,
    Real.rpow_def_of_pos (norm_pos_iff.mpr hz)]

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