English
For every real number r, the complex exponential of r equals the real exponential of r embedded into the complex numbers; equivalently, Complex.ofReal(exp_ℝ(r)) = exp_ℂ(C ofReal r).
Русский
Для каждого вещественного числа r комплексная экспонента от r совпадает с вещественной экспонентой от r после естественного вложения в комплексные числа; тождественно, Complex.ofReal(exp_ℝ(r)) = exp_ℂ(r).
LaTeX
$$$\\mathrm{Complex.ofReal}(\\exp_{\\mathbb{R}}(r)) = \\exp_{\\mathbb{C}}(r) \\quad (r \\in \\mathbb{R})$$$
Lean4
/-- A version of `Complex.ofReal_exp` for `NormedSpace.exp` instead of `Complex.exp` -/
@[simp, norm_cast]
theorem of_real_exp_ℝ_ℝ (r : ℝ) : ↑(exp ℝ r) = exp ℂ (r : ℂ) :=
(map_exp ℝ (algebraMap ℝ ℂ) (continuous_algebraMap _ _) r).trans (congr_fun exp_ℝ_ℂ_eq_exp_ℂ_ℂ _)
