ofReal_exp_ofReal_re — Mathlib

English

For real x, the real part of exp x (viewed in ℂ) equals exp x (the real exponential).

Русский

Для действительного x вещественная часть exp x (рассматриваемого как комплекс) равна exp x — действительному экспоненту.

LaTeX

$$$\\operatorname{Re}(\\exp x) = \\exp x \quad (x \\in \\mathbb{R})$$$

Lean4

@[simp]
theorem ofReal_exp_ofReal_re (x : ℝ) : ((exp x).re : ℂ) = exp x :=
  conj_eq_iff_re.1 <| by rw [← exp_conj, conj_ofReal]

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