norm_exp_ofReal

Mathlib.Analysis.Complex.Exponential

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

English

For every real x, the modulus of exp(x) equals e^x.

Русский

Для каждого вещественного x модуля экспоненты exp(x) равен e^x.

LaTeX

$$$\forall x \in \mathbb{R}, \|e^{x}\| = e^{x}$$$

Lean4

@[simp]
theorem norm_exp_ofReal (x : ℝ) : ‖exp x‖ = Real.exp x :=
  by
  rw [← ofReal_exp]
  exact Complex.norm_of_nonneg (le_of_lt (Real.exp_pos _))

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

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

Разделы

Аффилиация

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