isArtinianRing_iff_isFiniteLength

English

A ring R is Artinian if and only if it has finite length as a module over itself, i.e., IsArtinianRing R ⇔ IsFiniteLength R R.

Русский

Кольцо R является Artinian тогда и только тогда, когда оно имеет конечную длину как модуль над собой: IsArtinianRing R ⇔ IsFiniteLength R R.

LaTeX

$$$$\text{IsArtinianRing } R \iff \text{IsFiniteLength } R R.$$$$

Lean4

@[stacks 00JB "A ring is Artinian if and only if it has finite length as a module over itself."]
theorem isArtinianRing_iff_isFiniteLength : IsArtinianRing R ↔ IsFiniteLength R R :=
  ⟨fun h ↦ ((IsArtinianRing.tfae R R).out 2 3).mp h, fun h ↦ (isFiniteLength_iff_isNoetherian_isArtinian.mp h).2⟩

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