exp_smul_eps

Mathlib.Analysis.Normed.Algebra.DualNumber

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

English

For any scalar r, exp(r · ε) = 1 + r · ε in the DualNumber algebra.

Русский

Для любого скаляра r верна формула exp(r · ε) = 1 + r · ε в алгебре двойных чисел.

LaTeX

$$$\exp (r \cdot \varepsilon) = 1 + r \cdot \varepsilon$$$

Lean4

@[simp]
theorem exp_smul_eps (r : R) : exp 𝕜 (r • eps : DualNumber R) = 1 + r • eps := by rw [eps, ← inr_smul, exp_inr]

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

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

Разделы

Аффилиация

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