Theorem IsSemisimpleModule.exists_setIndependent_sSup_simples_eq_top

Modification history

2024-10-21 16:43
Mathlib/RingTheory/SimpleModule.lean
feat: semisimple rings are Artinian (#17557) …
Added IsSemisimpleModule.exists_setIndependent_sSup_simples_eq_topView on Github →