inv_cpow

Mathlib.Analysis.SpecialFunctions.Pow.Complex

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

English

For x ∈ ℂ and n ∈ ℂ, if arg(x) ≠ π, then x⁻¹^n = (x^n)⁻¹.

Русский

Для x ∈ ℂ и n ∈ ℂ, если arg(x) ≠ π, то x⁻¹^n = (x^n)⁻¹.

LaTeX

$$$x^{-1}^n = (x^n)^{-1}$, при arg(x) ≠ \pi$$

Lean4

theorem inv_cpow (x : ℂ) (n : ℂ) (hx : x.arg ≠ π) : x⁻¹ ^ n = (x ^ n)⁻¹ := by rw [inv_cpow_eq_ite, if_neg hx]

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

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

Разделы

Аффилиация

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