Instances related to Artinian rings #
We show that every reduced Artinian ring and the polynomial ring over it are decomposition monoids, and every reduced Artinian ring is semisimple.
theorem
StrongRankCondition.of_isArtinian
(R : Type u_1)
[Semiring R]
[Nontrivial R]
[∀ (n : ℕ), IsArtinian R (Fin n → R)]
:
If each Rⁿ is a Artinian R-module, then R satisfies the strong rank condition.
Not an instance for performance reasons.
instance
IsArtinianRing.instDecompositionMonoid
(R : Type u_1)
[CommRing R]
[IsArtinianRing R]
[IsReduced R]
:
instance
IsArtinianRing.instDecompositionMonoidPolynomial
(R : Type u_1)
[CommRing R]
[IsArtinianRing R]
[IsReduced R]
: