isNilpotent_eps

Mathlib.RingTheory.DualNumber

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

English

The element epsilon in the dual-number construction is nilpotent of order 2.

Русский

Элемент эпсилон в конструировании двойного числа нилпотент второго порядка.

LaTeX

$$$IsNilpotent(\\varepsilon) = true$$$

Lean4

theorem isNilpotent_eps [Semiring R] : IsNilpotent (ε : R[ε]) :=
  TrivSqZeroExt.isNilpotent_inr 1

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

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

Разделы

Аффилиация

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