commute_eps_right

Mathlib.Algebra.DualNumber

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

← MathLib Explorer

English

Equivalently, x commutes with ε for any x.

Русский

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

LaTeX

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

Lean4

/-- `ε` commutes with every element of the algebra. -/
theorem commute_eps_right [Semiring R] (x : DualNumber R) : Commute x ε :=
  (commute_eps_left x).symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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