IsArtinianRing — Mathlib

English

A ring is Artinian if and only if it is Artinian as a module over itself.

Русский

Кольцо является артинановым тогда и только тогда, когда оно артинаново как модуль над самим собой.

LaTeX

$$$ IsArtinian\\; Ring\\; R \\iff IsArtinian\\; R\\; R. $$$

Lean4

/-- A ring is Artinian if it is Artinian as a module over itself.

Strictly speaking, this should be called `IsLeftArtinianRing` but we omit the `Left` for
convenience in the commutative case. For a right Artinian ring, use `IsArtinian Rᵐᵒᵖ R`.

For equivalent definitions, see `Mathlib/RingTheory/Artinian/Ring.lean`.
-/
@[stacks 00J5]
abbrev IsArtinianRing (R) [Semiring R] :=
  IsArtinian R R

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