exp_conj — Mathlib

English

The exponential function commutes with complex conjugation: exp(conj x) = conj(exp x).

Русский

Экспонента коммутирует со сложением по сопряжению: exp(conj x) = conj(exp x).

LaTeX

$$$exp(conj x) = conj (exp x)$$$

Lean4

@[simp]
theorem exp_conj : exp (conj x) = conj (exp x) := by
  dsimp [exp]
  rw [← lim_conj]
  refine congr_arg CauSeq.lim (CauSeq.ext fun _ => ?_)
  dsimp [exp', Function.comp_def, cauSeqConj]
  rw [map_sum (starRingEnd _)]
  refine sum_congr rfl fun n _ => ?_
  rw [map_div₀, map_pow, ← ofReal_natCast, conj_ofReal]

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