cpow_conj

Mathlib.Analysis.SpecialFunctions.Pow.Complex

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

English

Let x ∈ ℂ, n ∈ ℂ with arg(x) ≠ π. Then x^{conj(n)} = conj( conj(x)^{n} ).

Русский

Пусть x ∈ ℂ, n ∈ ℂ и arg(x) ≠ π. Тогда x^{conj(n)} = conj( conj(x)^{n} ).

LaTeX

$$$$x^{\\overline{n}} = \\overline{\\overline{x}^{\\,n}}\\quad\\text{provided } \\arg(x) \\neq \\pi.$$$$

Lean4

theorem cpow_conj (x : ℂ) (n : ℂ) (hx : x.arg ≠ π) : x ^ conj n = conj (conj x ^ n) := by
  rw [conj_cpow _ _ hx, conj_conj]

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

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

Разделы

Аффилиация

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