mathlib3

a3b7241c - we may write a semisimple module as a product of simple submodules