Theorem IsSemisimpleRing.moduleEnd

Modification history

2025-11-16 21:05

Mathlib/RingTheory/SimpleModule/WedderburnArtin.lean

feat(RingTheory/SimpleModule): kill 4 proof_wanted on semisimple rings (#31672) …

Added IsSemisimpleRing.moduleEnd View on Github →