Theorem IsSemisimpleRing.exists_linearEquiv_ideal_of_isSimpleModule

Modification history

2025-11-16 21:05
Mathlib/RingTheory/SimpleModule/Basic.lean
feat(RingTheory/SimpleModule): kill 4 proof_wanted on semisimple rings (#31672) …
Added IsSemisimpleRing.exists_linearEquiv_ideal_of_isSimpleModuleView on Github →