Commit 2025-02-12 07:31 d066138f

feat(RingTheory): Hopkins–Levitzki theorem (#21451) RingTheory/HopkinsLevitzki.lean (new file): the Hopkins--Levitzki theorem says a module over a semiprimary ring is Noetherian iff it's Artinian (iff it's of finite length). As a consequence, a (left) Artinian ring is also (left) Noetherian, and a commutative ring is Artinian iff it's Noetherian and has Krull dimension 0. RingTheory/Jacobson/Semiprimary.lean (new file): contains the definition of semiprimary rings, and connections between Jacobson radicals of modules and semisimplicity. RingTheory/Jacobson/Radical.lean (new file): develop the theory of Jacobson radicals of modules, including versions of Nakayama's lemma over noncommutative rings. RingTheory/Artinian/Module.lean: show an Artinian module or ring is semisimple iff it has trivial radical; show that an Artinian ring is semiprimary.