proposition: Lemma gal_kAEndf (K E : {subfield L}) : (K <= E)%VS -> (gal E @* kAEndf K)%g = (gal E @* kAEnd K E)%g :> {set _}.
proof: Proof. move=> KE; rewrite kAEnd_split morphimIG ?ker_gal ?kAEndSl// (setIidPr _)//=. by rewrite (subset_trans (morphim_sub _ _))//= morphimS// subfield_closed. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)