norm_cpow_real

Mathlib.Analysis.SpecialFunctions.Pow.Real

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

English

For any complex x and real y, ∥x^{y}∥ = ∥x∥^{y}.

Русский

Для любого комплексного x и вещественного y выполняется ∥x^{y}∥ = ∥x∥^{y}.

LaTeX

$$$\|x^{y}\| = \|x\|^{y}$$$

Lean4

@[simp]
theorem norm_cpow_real (x : ℂ) (y : ℝ) : ‖x ^ (y : ℂ)‖ = ‖x‖ ^ y := by rw [norm_cpow_of_imp] <;> simp

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

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

Разделы

Аффилиация

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