Theorem IsSemisimpleModule.annihilator_isRadical

Modification history

2024-06-09 14:00
Mathlib/RingTheory/SimpleModule.lean
feat(Algebra, Order): simple submodules in a semisimple module (#13636) …
Modified IsSemisimpleModule.annihilator_isRadicalView on Github →
2024-03-05 01:29
Mathlib/RingTheory/SimpleModule.lean
feat: sum and product of commuting semisimple endomorphisms (#10808) …
Added IsSemisimpleModule.annihilator_isRadicalView on Github →