proposition: Lemma lker0_map_homE (f : 'End(L)) (x : L) : lker iota == 0%VS -> map_hom f (iota x) = iota (f x).
proof: Proof. by rewrite !comp_lfunE => /lker0_lfunK->. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)