jacobson_eq_nilradical_of_krullDimLE_zero

English

If R has Krull dimension zero, then the Jacobson radical equals the nilradical.

Русский

Если размерность Крull кольца R равна нулю, тогда якобсоновская радикал равна нильрадикалу.

LaTeX

$$$\text{Ring.KrullDimLE }0\;R \Rightarrow \mathrm{jacobson}(R) = \nilradical(R)$$$

Lean4

theorem jacobson_eq_nilradical_of_krullDimLE_zero (R) [CommRing R] [KrullDimLE 0 R] : jacobson R = nilradical R :=
  (nilradical_le_jacobson R).antisymm' <|
    nilradical_eq_sInf R ▸ le_sInf fun I (_ : I.IsPrime) ↦ sInf_le Ideal.IsMaximal.out

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