theorem semisimple_sub_smul_id {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (f : V →ₗ[K] V) (c : K) (hf : Module.End.IsSemisimple f) : (f - c • LinearMap.id).IsSemisimple