proposition: Lemma map_hom_is_linear : linear map_hom.
proof: Proof. move=> /= k a b; apply/lfunP => x; rewrite /map_hom. by rewrite !(comp_lfunE, add_lfunE, scale_lfunE) linearP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)