English
For any x ∈ ℂ and n ∈ ℂ, x⁻¹^n equals the piecewise expression: if x.arg = π then conj (x^conj n)⁻¹ else (x^n)⁻¹.
Русский
Для любых x ∈ ℂ и n ∈ ℂ, x⁻¹^n равно кусочно-зависимому выражению: если arg(x) = π, то conj(x^conj n)⁻¹, иначе (x^n)⁻¹.
LaTeX
$$$x^{-1}^n = \text{if } x.arg = \pi \text{ then } \overline{x ^ {\overline{n}}}^{-1} \text{ else } x^{-1^n}$$$
Lean4
theorem inv_cpow_eq_ite (x : ℂ) (n : ℂ) : x⁻¹ ^ n = if x.arg = π then conj (x ^ conj n)⁻¹ else (x ^ n)⁻¹ :=
by
simp_rw [Complex.cpow_def, log_inv_eq_ite, inv_eq_zero, map_eq_zero, ite_mul, neg_mul, RCLike.conj_inv,
apply_ite conj, apply_ite exp, apply_ite Inv.inv, map_zero, map_one, exp_neg, inv_one, inv_zero, ← exp_conj,
map_mul, conj_conj]
split_ifs with hx hn ha ha <;> rfl
