radical_eq_jacobson — Mathlib

English

For any ring R with IsJacobsonRing R, the radical equals Jacobson for all ideals I: I.radical = I.jacobson.

Русский

Для кольца R с IsJacobsonRing R радикал совпадает с радикалом Якобсона для любого идеала I: I.radical = I.jacobson.

LaTeX

$$$I.radical = I.jacobson$ for IsJacobsonRing R.$$

Lean4

theorem radical_eq_jacobson [H : IsJacobsonRing R] (I : Ideal R) : I.radical = I.jacobson :=
  le_antisymm (le_sInf fun _J ⟨hJ, hJ_max⟩ => (IsPrime.radical_le_iff hJ_max.isPrime).mpr hJ)
    (H.out (radical_isRadical I) ▸ jacobson_mono le_radical)

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