isNilpotent_iff_mem_nonunits

Mathlib.RingTheory.KrullDimension.Zero

URI: https://scilib.ai/kg/mathlib#Ring.KrullDimLE.isNilpotent_iff_mem_nonunits

English

In a local ring R, x is nilpotent if and only if x is a nonunit.

Русский

В локальном кольце R элемент x является nilpotent, если и только если он не является единицей (необратимым).

LaTeX

$$$IsNilpotent(x) \\iff x \\in \\text{nonunits }R$$$

Lean4

theorem isNilpotent_iff_mem_nonunits [IsLocalRing R] {x} : IsNilpotent x ↔ x ∈ nonunits R :=
  isNilpotent_iff_mem_maximalIdeal

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

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

Разделы

Аффилиация

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