proposition: Lemma normalClosure_normal E F : normalField E (normalClosure E F).
proof: Proof. apply/'forall_implyP => s s_end; apply/eqP. rewrite /normalClosure (big_morph _ (aimgM _) (aimg1 _)). under eq_bigr => s' do rewrite -limg_comp. under eq_bigr => s' do have -> : (s \o s')%VF = 'R%act s' s by []. have /(reindex_astabs 'R _) : s \in ('N(kAEndf E | 'R))%g by rewrite astabsR/=. by move/(_ _ _ _ (fun i => i @: (E * F))%AS); rewrite !big_prodv_eq_aspace => <-. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)