proposition: Lemma kAEnd_split (K E : {subfield L}) : kAEnd K E = kAEnd 1 E :&: kAEndf K.
proof: Proof. apply/setP => f; rewrite !inE kAut1E !kAutE subvf andbT andbC. by case fE : (f @: E <= E)%VS => //=; apply/kAHomP/kAHomP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)