proposition: Lemma lker_ker phi : lker phi = vsof e (kermx (mxof e e phi)).
proof: Proof. apply/vspaceP => v; rewrite memv_ker -rowmxof_sub// (sameP sub_kermxP eqP). by rewrite -rowmxof_app// rowmxof_eq0. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra all_solvable)