Theorem IsSemisimpleModule.exists_end_algEquiv

Modification history

2025-11-16 21:05
Mathlib/RingTheory/SimpleModule/WedderburnArtin.lean
feat(RingTheory/SimpleModule): kill 4 proof_wanted on semisimple rings (#31672) …
Deleted IsSemisimpleModule.exists_end_algEquivView on Github →
2025-08-14 04:35
Mathlib/RingTheory/SimpleModule/WedderburnArtin.lean
feat(RingTheory): semisimple Wedderburn–Artin existence (#24192)
Added IsSemisimpleModule.exists_end_algEquivView on Github →