jacobson_eq_radical — Mathlib

English

In a commutative Artinian ring, the Jacobson radical of any ideal I coincides with its radical: I.jacobson = I.radical.

Русский

В коммутативном артиниановом кольце радикал Джейкобсона любого идеала I совпадает с его радикалом: I.jacobson = I.radical.

LaTeX

$$$\forall I \in \mathrm{Ideal}(R),\ I.jacobson = I.radical$$$

Lean4

theorem jacobson_eq_radical (I : Ideal R) : I.jacobson = I.radical := by
  simp_rw [Ideal.jacobson, Ideal.radical_eq_sInf, IsArtinianRing.isPrime_iff_isMaximal]

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