isNilpotent_jacobson_bot — Mathlib

English

In an Artinian ring R, the Jacobson radical of the zero ideal is nilpotent.

Русский

В артиновском кольце R радикал Джейкобсона нулевого идеала является нильпотентным.

LaTeX

$$$\exists n \in \mathbb{N},\ (Ideal.jacobson(\bot))^n = \bot$$$

Lean4

@[stacks 00J8]
theorem isNilpotent_jacobson_bot {R} [Ring R] [IsArtinianRing R] : IsNilpotent (Ideal.jacobson (⊥ : Ideal R)) :=
  Ideal.jacobson_bot (R := R) ▸ IsSemiprimaryRing.isNilpotent

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