proposition: Lemma charf_p_separable K x e p : p \in [char L] -> separable_element K x = (x \in <<K; x ^+ (p ^ e.+1)>>%VS).
proof: Proof. move=> charLp; apply/idP/idP=> [sepKx | /Fadjoin_poly_eq]; last first. set m := p ^ _; set f := Fadjoin_poly K _ x => Dx; apply/separable_elementP. have mL0: m%:R = 0 :> L by apply/eqP; rewrite -(dvdn_charf charLp) dvdn_exp. exists ('X - (f \Po 'X^m)); split. - by rewrite rpredB ?polyOver_comp ?rpredX ?polyOverX ?Fadjoin_polyOver. - by rewrite rootE !hornerE horner_comp hornerXn Dx subrr. rewrite unlock !(derivE, deriv_comp) -mulr_natr -rmorphMn /= mL0. by rewrite !mulr0 subr0 coprimep1. without loss{e} ->: e x sepKx / e = 0. move=> IH; elim: {e}e.+1 => [|e]; [exact: memv_adjoin | apply: subvP]. apply/FadjoinP/andP; rewrite subv_adjoin expnSr exprM (IH 0) //. by have /adjoin_separableP-> := sepKx; rewrite ?rpredX ?memv_adjoin. set K' := <<K; x ^+ p>>%VS; have sKK': (K <= K')%VS := subv_adjoin _ _. pose q := minPoly K' x; pose g := 'X^p - (x ^+ p)%:P. have [K'g]: g \is a polyOver K' /\ q \is a polyOver K'. by rewrite minPolyOver rpredB ?rpredX ?polyOverX // polyOverC memv_adjoin. have /dvdpP[c Dq]: 'X - x%:P %| q by rewrite dvdp_XsubCl root_minPoly. have co_c_g: coprimep c g. have charPp: p \in [char {poly L}] := rmorph_char polyC charLp. rewrite /g polyC_exp -!(Frobenius_autE charPp) -rmorphB coprimep_expr //. have: separable_poly q := separable_elementS sKK' sepKx. by rewrite Dq separable_mul => /and3P[]. have{g K'g co_c_g} /size_poly1P[a nz_a Dc]: size c == 1. suffices c_dv_g: c %| g by rewrite -(eqp_size (dvdp_gcd_idl c_dv_g)). have: q %| g by rewrite minPoly_dvdp // rootE !hornerE subrr. by apply: dvdp_trans; rewrite Dq dvdp_mulIl. rewrite {q}Dq {c}Dc mulrBr -rmorphM -rmorphN -cons_poly_def qualifE /=. by rewrite polyseq_cons !polyseqC nz_a /= rpredN andbCA => /and3P[/fpredMl->]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop finset prime) mathcomp(binomial ssralg poly polydiv fingroup perm) mathcomp(morphism quotient gproduct finalg zmodp cyclic) mathcomp(matrix mxalgebra mxpoly polyXY vector falgebra) mathcomp(fieldext)