Theorem RingEquiv.isSemisimpleRing

Modification history

2025-08-13 09:52

Mathlib/RingTheory/SimpleModule/Basic.lean

chore(RingTheory): use `extend` instead of `abbrev` in `IsS(emis)impleModule` (#27427)

Modified RingEquiv.isSemisimpleRing View on Github →

2024-03-05 01:29

Mathlib/RingTheory/SimpleModule.lean

feat: sum and product of commuting semisimple endomorphisms (#10808) …

Added RingEquiv.isSemisimpleRing View on Github →