isArtinianRing_iff_krullDimLE_zero

English

Under Noetherian hypothesis, a ring is Artinian if and only if its Krull dimension is zero.

Русский

При условии Noetherian кольца, Artinian ⇔ KrullDimLE 0.

LaTeX

$$$$\text{If } [\text{CommRing } R], [\text{IsNoetherianRing } R], \text{ then } \operatorname{IsArtinianRing} R \iff \operatorname{Ring.KrullDimLE} 0 R.$$$$

Lean4

theorem isArtinianRing_iff_krullDimLE_zero {R : Type*} [CommRing R] [IsNoetherianRing R] :
    IsArtinianRing R ↔ Ring.KrullDimLE 0 R := by
  rwa [isArtinianRing_iff_isNoetherianRing_krullDimLE_zero, and_iff_right]

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