proposition: Fact galLgen K : {alpha | generator 'Gal({:L} / K) alpha & forall x, alpha x = x ^+ order K}.
proof: Proof. without loss{K} ->: K / K = 1%AS; last rewrite /order dimv1 expn1. case/(_ 1%AS)=> // alpha /eqP-defGalL; rewrite /order dimv1 expn1 => Dalpha. exists (alpha ^+ \dim K)%g => [|x]; last first. elim: (\dim K) => [|n IHn]; first by rewrite gal_id. by rewrite expgSr galM ?memvf // IHn Dalpha expnSr exprM. have sGalLK: 'Gal({:L} / K) \subset <[alpha]> by rewrite -defGalL galS ?sub1v. rewrite /generator {sGalLK}(eq_subG_cyclic _ sGalLK) ?cycle_cyclic ?cycleX //. rewrite -orderE orderXdiv orderE -defGalL -?{1}galois_dim ?dimv1 ?divn1 //. by rewrite field_dimS ?subvf. pose f x := x ^+ #|F|. have idfP x: reflect (f x = x) (x \in 1%VS). apply: (iffP (vlineP _ _)) => [[a ->] | xFx]. by rewrite -in_algE -[LHS]rmorphXn expf_card. pose q := map_poly (in_alg L) ('X^#|F| - 'X). have: root q x. rewrite /q rmorphB /= map_polyXn map_polyX. by rewrite rootE !(hornerE, hornerXn) [x ^+ _]xFx subrr. have{q} ->: q = \prod_(z <- [seq b%:A | b : F]) ('X - z%:P). rewrite /q finField_genPoly rmorph_prod big_image /=. by apply: eq_bigr => b _; rewrite rmorphB /= map_polyX map_polyC. by rewrite root_prod_XsubC => /mapP[a]; exists a. have fA : additive f. rewrite /f => x y; rewrite ?exprMn ?expr1n //. have [p _ charFp] := finCharP F; rewrite (card_primeChar charFp). elim: (logn _ _) => // n IHn; rewrite expnSr !exprM {}IHn. by rewrite -(char_lalg L) in charFp; rewrite -Frobenius_autE rmorphB. have fM : multiplicative f. by rewrite /f; split=> [x y|]; rewrite ?exprMn ?expr1n //. have fZ: scalable f. move=> a x; rewrite -[in LHS]mulr_algl fM. by rewrite (idfP _ _) ?mulr_algl ?memvZ // memv_line. pose faM := GRing.isAdditive.Build _ _ f fA. pose fmM := GRing.isMultiplicative.Build _ _ f fM. pose flM := GRing.isScalable.Build _ _ _ _ f fZ. pose fLRM : {lrmorphism _ -> _} := HB.pack f faM fmM flM. have /kAut_to_gal[alpha galLalpha Dalpha]: kAut 1 {:L} (linfun fLRM). rewrite kAutfE; apply/kHomP; split=> [x y _ _ | x /idfP]; rewrite !lfunE //=. exact: (rmorphM fLRM). have{} Dalpha: alpha =1 f by move=> a; rewrite -Dalpha ?memvf ?lfunE. suffices <-: fixedField [set alpha] = 1%AS. by rewrite gal_generated /generator; exists alpha. apply/vspaceP=> x; apply/fixedFieldP/idfP; rewrite ?memvf // => id_x. by rewrite -Dalpha id_x ?set11. by move=> _ /set1P->; rewrite Dalpha. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype div tuple bigop prime finset fingroup) mathcomp(ssralg poly polydiv morphism action countalg) mathcomp(finalg zmodp cyclic center pgroup abelian matrix) mathcomp(mxpoly vector falgebra fieldext separable galois)