zero

Mathlib.RingTheory.Nilpotent.Defs

URI: https://scilib.ai/kg/mathlib#IsNilpotent.zero

English

The zero element is nilpotent.

Русский

Нулевой элемент нилпотентен.

LaTeX

$$$\\IsNilpotent(0)$$$

Lean4

@[simp]
theorem zero [MonoidWithZero R] : IsNilpotent (0 : R) :=
  ⟨1, pow_one 0⟩

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

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

Разделы

Аффилиация

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