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] :