English
If R is Jacobson, then the generic MvPolynomial over R is Jacobson.
Русский
Если R — кольцо Якобсона, то многочлены MvPolynomial над R тоже Якобсон.
LaTeX
$$IsJacobsonRing (MvPolynomial ι R)$$
Lean4
/-- General form of the Nullstellensatz for Jacobson rings, since in a Jacobson ring we have
`Inf {P maximal | P ≥ I} = Inf {P prime | P ≥ I} = I.radical`. Fields are always Jacobson,
and in that special case this is (most of) the classical Nullstellensatz,
since `I(V(I))` is the intersection of maximal ideals containing `I`, which is then `I.radical` -/
instance isJacobsonRing {R : Type*} [CommRing R] {ι : Type*} [Finite ι] [IsJacobsonRing R] :
IsJacobsonRing (MvPolynomial ι R) := by
cases nonempty_fintype ι
let e := Fintype.equivFin ι
rw [isJacobsonRing_iso (renameEquiv R e).toRingEquiv]
exact isJacobsonRing_MvPolynomial_fin _
