isNilpotent_nilradical — Mathlib

English

In a commutative Noetherian ring, the nilradical is nilpotent.

Русский

В коммутативном Нётеровом кольце нильрадикал нильпотентен.

LaTeX

$$$R\\text{ commutative}, \\text{IsNoetherianRing}(R) \\Rightarrow \\text{IsNilpotent}(\\nilradical(R))$$$

Lean4

theorem isNilpotent_nilradical (R : Type*) [CommSemiring R] [IsNoetherianRing R] : IsNilpotent (nilradical R) :=
  by
  obtain ⟨n, hn⟩ := Ideal.exists_radical_pow_le_of_fg (⊥ : Ideal R) (IsNoetherian.noetherian _)
  exact ⟨n, eq_bot_iff.mpr hn⟩

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