conj_cpow_eq_ite — Mathlib

English

For x ∈ ℂ and n ∈ ℂ, conj x ^ n equals x^n if arg(x) = π, otherwise conj(x^conj n).

Русский

Для x ∈ ℂ и n ∈ ℂ, conj x ^ n равно x^n, если arg(x) = π, иначе conj(x^conj n).

LaTeX

$$$\operatorname{conj}(x)^{n} = \begin{cases} x^{n} & (x.arg = \pi) \\ conj(x^{conj n}) & \text{иначе} \end{cases}$$$

Lean4

theorem conj_cpow_eq_ite (x : ℂ) (n : ℂ) : conj x ^ n = if x.arg = π then x ^ n else conj (x ^ conj n) :=
  by
  simp_rw [cpow_def, map_eq_zero, apply_ite conj, map_one, map_zero, ← exp_conj, map_mul, conj_conj, log_conj_eq_ite]
  split_ifs with hcx hn hx <;> rfl

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