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.

instance IsArtinianRing.instDecompositionMonoid (R : Type u_1) [CommRing R] [IsArtinianRing R] [IsReduced R] : DecompositionMonoid R

instance IsArtinianRing.instDecompositionMonoidPolynomial (R : Type u_1) [CommRing R] [IsArtinianRing R] [IsReduced R] : DecompositionMonoid (Polynomial R)

theorem IsArtinianRing.isSemisimpleRing_of_isReduced (R : Type u_1) [CommRing R] [IsArtinianRing R] [IsReduced R] : IsSemisimpleRing R