eps_mul_eps

Mathlib.Algebra.DualNumber

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

English

The square of the infinitesimal ε is zero in any semiring extension.

Русский

Квадрат бесконечно малого элемента ε равен нулю во всех полях расширения полей.

LaTeX

$$$\varepsilon \cdot \varepsilon = 0$$$

Lean4

@[simp]
theorem eps_mul_eps [Semiring R] : (ε * ε : R[ε]) = 0 :=
  inr_mul_inr _ _ _

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

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

Разделы

Аффилиация

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