log_conj_eq_ite — Mathlib

English

log(conj x) = if arg x = π then log x else conj(log x).

Русский

log(conj x) = если arg x = π то log x, иначе conj(log x).

LaTeX

$$$\log(\overline{x}) = \begin{cases} \log x, & \arg x = \pi \\ \overline{\log x}, & \text{иначе} \end{cases}$$$

Lean4

theorem log_conj_eq_ite (x : ℂ) : log (conj x) = if x.arg = π then log x else conj (log x) :=
  by
  simp_rw [log, norm_conj, arg_conj, map_add, map_mul, conj_ofReal]
  split_ifs with hx
  · rw [hx]
  simp_rw [ofReal_neg, conj_I, mul_neg, neg_mul]

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