out — Mathlib

English

From the isJacobsonRing_iff_prime_eq, one obtains that IsJacobsonRing R implies for every radical ideal I, I.jacobson = I.

Русский

Из изоморфного утверждения IsJacobsonRing следует, что для каждого радикального идеала I выполняется I.jacobson = I.

LaTeX

$$IsJacobsonRing.out : IsJacobsonRing R → ∀{I}, I.IsRadical → I.jacobson = I$$

Lean4

theorem out {R} [CommRing R] : IsJacobsonRing R → ∀ {I : Ideal R}, I.IsRadical → I.jacobson = I :=
  isJacobsonRing_iff.1

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