Commit 2024-10-21 16:43 ff8e6e85

feat: semisimple rings are Artinian (#17557) The main result IsSemisimpleModule.finite_tfae shows that for a semisimple module, Module.Finite R M ↔ IsNoetherian R M ↔ IsArtinian R M ↔ IsFiniteLength R M ↔ direct sum decomposition into finitely many simple modules (F25 in Chapter 28 of Lorenz's Algebra II). The instance from IsSemisimpleModule + Module.Finite to IsNoetherian is proven before and used in the proof, while the instance to IsArtinian is added after the proof. As a consequence, semisimple rings are Artinian. Also add easy lemmas isNoetherian_range, LinearEquiv.isNoetherian_iff, isNoetherian_sup, isNoetherian_iSup (and Artinian counterparts) and IsSemisimpleModule.exists_setIndependent_sSup_simples_eq_top.