proposition: Lemma normalFieldP K E : reflect {in E, forall a, exists2 r, all [in E] r & minPoly K a = \prod_(b <- r) ('X - b%:P)} (normalField K E).
proof: Proof. apply: (iffP eqfun_inP) => [nKE a Ea | nKE x]; last first. rewrite inE kAutfE => homKx; suffices: kAut K E x by case/andP=> _ /eqP. rewrite kAutE (kHomSr (subvf E)) //=; apply/subvP=> _ /memv_imgP[a Ea ->]. have [r /allP/=srE splitEa] := nKE a Ea. rewrite srE // -root_prod_XsubC -splitEa. by rewrite -(kHom_poly_id homKx (minPolyOver K a)) fmorph_root root_minPoly. have [r /eqP splitKa] := splitting_field_normal K a. exists r => //; apply/allP => b; rewrite -root_prod_XsubC -splitKa => pKa_b_0. pose y := kHomExtend K \1 a b; have [hom1K lf1p] := (kHom1 K K, lfun1_poly). have homKy: kHom K <<K; a>> y by apply/kHomExtendP; rewrite ?lf1p. have [[g Dy] [_ idKy]] := (kHom_to_AEnd homKy, kHomP homKy). have <-: g a = b by rewrite -Dy ?memv_adjoin // (kHomExtend_val hom1K) ?lf1p. suffices /nKE <-: g \in kAEndf K by apply: memv_img. by rewrite inE kAutfE; apply/kAHomP=> c Kc; rewrite -Dy ?subvP_adjoin ?idKy. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg poly) mathcomp(polydiv finset fingroup morphism quotient perm) mathcomp(action zmodp cyclic matrix mxalgebra vector) mathcomp(falgebra fieldext separable)