Theorem IsArtinianRing.isSemisimpleRing_of_isReduced
Modification history
2025-02-12 07:31
Mathlib/RingTheory/Artinian/Instances.lean
feat(RingTheory): Hopkins–Levitzki theorem (#21451) …
Modified IsArtinianRing.isSemisimpleRing_of_isReducedView on Github →