instIsArtinianRingQuotientIdeal — Mathlib

English

If R is Artinian and I is a two-sided ideal, then the quotient ring R/I is Artinian.

Русский

Если R артинаново как кольцо и I — двусторонний идеал, то R/I артинаново.

LaTeX

$$$ IsArtinianRing\\; R \\Rightarrow [I.IsTwoSided]\\Rightarrow IsArtinianRing\\; (R/I). $$$

Lean4

instance (R) [Ring R] [IsArtinianRing R] (I : Ideal R) [I.IsTwoSided] : IsArtinianRing (R ⧸ I) :=
  isArtinian_of_tower R inferInstance

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