isNilpotent_nilradical

Mathlib.RingTheory.Artinian.Ring

URI: https://scilib.ai/kg/mathlib#IsArtinianRing.isNilpotent_nilradical

English

In an Artinian ring R, the nilradical is nilpotent.

Русский

В артиниановом кольце R нильрадикал является нильпотентным.

LaTeX

$$$\exists n \in \mathbb{N},\ nilradical(R)^n = \bot$$$

Lean4

theorem isNilpotent_nilradical : IsNilpotent (nilradical R) :=
  by
  rw [nilradical, ← jacobson_eq_radical]
  exact isNilpotent_jacobson_bot

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

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

Разделы

Аффилиация

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