norm_cpow_inv_nat

Mathlib.Analysis.SpecialFunctions.Pow.Real

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

English

For a complex number x and a natural n, ∥x^{n^{-1}}∥ = ∥x∥^{n^{-1}}.

Русский

Для комплексного числа x и натурального числа n выполняется ∥x^{n^{-1}}∥ = ∥x∥^{n^{-1}}.

LaTeX

$$$\|x^{n^{-1}}\| = \|x\|^{n^{-1}}$$$

Lean4

@[simp]
theorem norm_cpow_inv_nat (x : ℂ) (n : ℕ) : ‖x ^ (n⁻¹ : ℂ)‖ = ‖x‖ ^ (n⁻¹ : ℝ) := by rw [← norm_cpow_real]; simp

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

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

Разделы

Аффилиация

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