exp_eps

Mathlib.Analysis.Normed.Algebra.DualNumber

URI: https://scilib.ai/kg/mathlib#DualNumber.exp_eps

English

In the DualNumber algebra, the exponential of the infinitesimal ε equals 1 + ε.

Русский

В алгебре двойных чисел экспонента от бесконечно малой ε равна 1 + ε.

LaTeX

$$$\exp 𝕜 (\varepsilon) = 1 + \varepsilon$$$

Lean4

@[simp]
theorem exp_eps : exp 𝕜 (eps : DualNumber R) = 1 + eps :=
  exp_inr _ _

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

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

Разделы

Аффилиация

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