English
Let x be a nonzero complex number with argument not equal to π, and let n be any complex number. Then the complex conjugate of x raised to the power n equals the conjugate of x raised to the conjugate of n: overline(x)^n = overline( x^{ overline(n) } ).
Русский
Пусть x ∈ ℂ с arg(x) ≠ π и n ∈ ℂ. Тогда сопряжение числа x в степени n удовлетворяет надлежащему правилу: \n\\overline{x}^n = \\overline{ x^{\\overline{n}} }.
LaTeX
$$$$\\text{Let } x \\in \\mathbb{C},\\ n \\in \\mathbb{C},\\ \\arg(x) \\neq \\pi.\\quad \\overline{x}^{\\,n} = \\overline{\\,x^{\\,\\overline{n}}}\\,.$$$$
Lean4
theorem conj_cpow (x : ℂ) (n : ℂ) (hx : x.arg ≠ π) : conj x ^ n = conj (x ^ conj n) := by
rw [conj_cpow_eq_ite, if_neg hx]
