proposition: Lemma separable_aimgr E F s : s \in kAEndf E -> separable E (s @: F) = separable E F.
proof: Proof. rewrite inE => /kHom_kAut_sub/kAHomP s_id; rewrite -[RHS](separable_aimg _ _ s). suff /eq_in_limg->: {in E, s =1 \1%VF} by rewrite lim1g. by move=> x xE; rewrite lfunE/= s_id. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)