commute_eps_left

Mathlib.Algebra.DualNumber

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

English

The infinitesimal ε commutes with every element of the algebra.

Русский

Бесконечно малый элемент ε коммутирует с любым элементом алгебры.

LaTeX

$$$\forall x:\text{DualNumber }R, \; \varepsilon x = x \varepsilon$$$

Lean4

/-- `ε` commutes with every element of the algebra. -/
theorem commute_eps_left [Semiring R] (x : DualNumber R) : Commute ε x := by ext <;> simp

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

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

Разделы

Аффилиация

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