∀ {M : Type u_2} [inst : AddCommGroup M] {K : Type u_3} [inst_1 : Field K] [inst_2 : Module K M] {f g : Module.End K M}
  [FiniteDimensional K M] [PerfectField K], Commute f g → f.IsSemisimple → g.IsSemisimple → (f * g).IsSemisimple