Finite-dimensional simple algebra is semisimple (source code)

= Finite-dimensional simple algebra is semisimple

For a nonzero <associative algebra> $A$ of finite <dimension> that is a <simple ring>, choose a <minimal left ideal> $I$. Right multiplication $I\to Ia$ is a <module homomorphism>, so $Ia$ is zero or a <simple module>. The sum $\sum_{a\in A}Ia$ is a nonzero <two-sided ideal>, hence $A$. Finite <dimension> reduces this to a finite sum. The <finite sum of simple submodules> lemma shows that the <left regular module> is a <semisimple module>.