norm_natCast_cpow_of_re_ne_zero — Mathlib

English

For a natural n with Re(s) ≠ 0, ∥(n^s)∥ = n^{Re s}.

Русский

Для натурального n и s с Re(s) ≠ 0, ∥(n^s)∥ = n^{Re s}.

LaTeX

$$$n \in \mathbb{N},\ s \in \mathbb{C},\ Re(s) \neq 0 \Rightarrow \| (n:\mathbb{C})^{s} \| = (n:\mathbb{R})^{\Re s}$$$

Lean4

theorem norm_natCast_cpow_of_re_ne_zero (n : ℕ) {s : ℂ} (hs : s.re ≠ 0) : ‖(n : ℂ) ^ s‖ = (n : ℝ) ^ (s.re) := by
  rw [← ofReal_natCast, norm_cpow_eq_rpow_re_of_nonneg n.cast_nonneg hs]

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