Commit 2025-11-16 21:05 45368db4

feat(RingTheory/SimpleModule): kill 4 proof_wanted on semisimple rings (#31672) Prove that

• the opposite of a semisimple ring is semisimple,
• the endomorphism ring of a finite semisimple module is semisimple,
• matrix rings over a semisimple ring are semisimple (these are opposites of endomorphism rings of finite free modules);
• finite products of matrix rings over division rings are semisimple (the easy direction of Wedderburn–Artin; the hard direction was already in mathlib).