proposition: Lemma leigenspaceE f a : leigenspace f a = vsof e (eigenspace (mxof e e f) a).
proof: Proof. by rewrite /leigenspace /eigenspace lker_ker linearB linearZ/= mxof1// scalemx1. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra all_solvable)