eq_zero

Mathlib.RingTheory.Nilpotent.Defs

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

English

If IsNilpotent x then x = 0.

Русский

Если x нильпотентен, то x = 0.

LaTeX

$$$\mathrm{IsNilpotent}(x) \Rightarrow x = 0$$$

Lean4

theorem eq_zero [Zero R] [Pow R ℕ] [IsReduced R] (h : IsNilpotent x) : x = 0 :=
  IsReduced.eq_zero x h

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

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

Разделы

Аффилиация

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