isNilpotent_iff_le_nilradical — Mathlib

English

For a finitely generated ideal I in a commutative ring, I is nilpotent if and only if I is contained in the nilradical.

Русский

Для FG-идеала I в коммутативном кольце: I нильпотентен тогда и только тогда, когда I ⊆ nilradical(R).

LaTeX

$$$\\forall R, [CommSemiring R] \\Rightarrow \\forall I:\\text{Ideal }R, I.FG \\Rightarrow (IsNilpotent I \\iff I \\le \\nilradical R)$$$

Lean4

theorem isNilpotent_iff_le_nilradical {R : Type*} [CommSemiring R] {I : Ideal R} (hI : I.FG) :
    IsNilpotent I ↔ I ≤ nilradical R :=
  ⟨fun ⟨n, hn⟩ _ hx ↦ ⟨n, hn ▸ Ideal.pow_mem_pow hx n⟩, fun h ↦
    let ⟨n, hn⟩ := exists_pow_le_of_le_radical_of_fg h hI;
    ⟨n, le_bot_iff.mp hn⟩⟩

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