Commit 2025-02-07 18:54 2e4bea35

feat: Prerequisites for Hopkins–Levitzki theorem (#21544) RingTheory/HopkinsLevitzki.lean requires:

• Order/Atoms.lean, RingTheory/Ideal/Operations.lean: show two distinct maximal ideals are coprime (comaximal).
• RingTheory/Ideal/Maps.lean: add two lemmas about annihilators.
• Algebra/Module/Torsion.lean: add a lemma about being a semisimple module over a quotient ring.
• RingTheory/KrullDimension/Basic.lean: add lemmas about zero-dimensional rings.
• RingTheory/Spectrum/Prime/Topology.lean: switch to Ring.KrullDimLE. RingTheory/Jacobson/Radical.lean requires:
• Algebra/Module/Submodule/Map.lean and LinearAlgebra/Span/Basic.lean: Lemmas used to show functoriality of Jacobson radical of modules (le_comap_jacobson). RingTheory/SimpleModule.lean: split out a single lemma that requires Module.finrank to reduce imports: SimpleModule.lean is renamed SimpleModule/Basic.lean, and the lemma is moved into SimpleModule/Rank.lean.
• LinearAlgebra/DFinsupp.lean: add lemmas to show a direct sum of semisimple modules is semisimple. RingTheory/Artinian/Module.lean requires:
• RingTheory/Artinian/Instances.lean: move an instance to Artinian/Module, which now imports SimpleModule.
• Data/Finset/Lattice/Fold.lean: add lemmas used to golf IsArtinianRing.setOf_isMaximal_finite and in the proof of that an Artinian ring is semiprimary.