instIsNoetherianRingOfIsArtinianRing

English

If R is Artinian, then it is Noetherian as a ring, i.e., IsArtinianRing R ⇒ IsNoetherianRing R.

Русский

Если R Artinian, то R является Noetherian кольцом: IsArtinianRing R ⇒ IsNoetherianRing R.

LaTeX

$$$$\operatorname{IsArtinianRing} R \Rightarrow \operatorname{IsNoetherianRing} R.$$$$

Lean4

@[stacks 00JB "A ring is Artinian if and only if it has finite length as a module over itself.
      **Any such ring is both Artinian and Noetherian.**"]
instance [IsArtinianRing R] : IsNoetherianRing R :=
  ((IsArtinianRing.tfae R R).out 2 1).mp ‹_›

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