exp_ℝ_ℂ_eq_exp_ℂ_ℂ — Mathlib

English

The exponential function on the complex numbers defined via the real field agrees with the standard complex exponential; i.e. exp_ℝ = exp_ℂ as functions ℂ → ℂ.

Русский

Экспоненциальная функция над комплексными числами, определяемая через действительное основание, совпадает с обычной комплексной экспонентой; то есть exp_ℝ = exp_ℂ как отображения ℂ → ℂ.

LaTeX

$$$\\exp_{\\mathbb{R}} = \\exp_{\\mathbb{C}}$ on $\\mathbb{C}$$$

Lean4

theorem exp_ℝ_ℂ_eq_exp_ℂ_ℂ : (exp ℝ : ℂ → ℂ) = exp ℂ :=
  exp_eq_exp ℝ ℂ ℂ

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