ofReal_exp

Mathlib.Analysis.Complex.Exponential

URI: https://scilib.ai/kg/mathlib#Complex.ofReal_exp

English

For real x, (Real.exp x) as a complex number equals exp(Real.ofReal x).

Русский

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

LaTeX

$$$(\\text{Real.exp } x) \\text{ как элемент } \\mathbb{C} = \\exp(\\text{ofReal } x)$$$

Lean4

@[simp, norm_cast]
theorem ofReal_exp (x : ℝ) : (Real.exp x : ℂ) = exp x :=
  ofReal_exp_ofReal_re _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru