norm_cpow_eq_rpow_re_of_nonneg

Mathlib.Analysis.SpecialFunctions.Pow.Real

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

← MathLib Explorer

English

Let x ≥ 0 and y ∈ ℂ with Re(y) ≠ 0; then ∥(x)^y∥ = x^{Re y}.

Русский

Пусть x ≥ 0 и y ∈ ℂ с Re(y) ≠ 0; тогда ∥x^y∥ = x^{Re y}.

LaTeX

$$$x \ge 0 \Rightarrow \Re(y) \neq 0 \Rightarrow \|x^{y}\| = x^{\Re y}$$$

Lean4

theorem norm_cpow_eq_rpow_re_of_nonneg {x : ℝ} (hx : 0 ≤ x) {y : ℂ} (hy : re y ≠ 0) : ‖(x : ℂ) ^ y‖ = x ^ re y := by
  rw [norm_cpow_of_imp] <;> simp [*, arg_ofReal_of_nonneg, abs_of_nonneg]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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