exp — Mathlib

English

The real exponential function is defined as the real part of the complex exponential: Real.exp(x) = Re( Complex.exp( Complex.ofReal(x) ) ).

Русский

Реальная экспонента определяется как вещественная часть комплексной экспоненты: Real.exp(x) = Re( Complex.exp( Complex.ofReal(x) ) ).

LaTeX

$$$\\operatorname{Real\\;exp}(x) = \\Re\\big( \\operatorname{Complex\\;exp}(\\operatorname{Complex\\;ofReal}(x)) \\big)$$$

Lean4

/-- The real exponential function, defined as the real part of the complex exponential -/
@[pp_nodot]
nonrec def exp (x : ℝ) : ℝ :=
  (exp x).re

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