instJacobsonSpaceCarrierCarrierCommRingCatSpecOfOfIsJacobsonRing

English

If R is a Jacobson ring, then Spec R is a Jacobson space.

Русский

Если R — кольцо Джейкобсона, то спектр Spec R является пространством Джейкобсона.

LaTeX

$$$\\text{CommRing}(R) \\wedge \\text{IsJacobsonRing}(R) \\;\Rightarrow\\; \\text{JacobsonSpace}(\\Spec R)$$$

Lean4

instance {R} [CommRing R] [IsJacobsonRing R] : JacobsonSpace <| Spec <| .of R :=
  inferInstanceAs (JacobsonSpace (PrimeSpectrum R))

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