proposition: Lemma separablePn : reflect (exists2 p, p \in [char L] & exists2 g, g \is a polyOver K & minPoly K x = g \Po 'X^p) (~~ separable_element K x).
proof: Proof. rewrite separable_nz_der negbK; set f := minPoly K x. apply: (iffP eqP) => [f'0 | [p Hp [g _ ->]]]; last first. by rewrite deriv_comp derivXn -scaler_nat (charf0 Hp) scale0r mulr0. pose n := adjoin_degree K x; have sz_f: size f = n.+1 := size_minPoly K x. have fn1: f`_n = 1 by rewrite -(monicP (monic_minPoly K x)) lead_coefE sz_f. have dimKx: (adjoin_degree K x)%:R == 0 :> L. by rewrite -(coef0 _ n.-1) -f'0 coef_deriv fn1. have /natf0_char[// | p charLp] := dimKx. have /dvdnP[r Dn]: (p %| n)%N by rewrite (dvdn_charf charLp). exists p => //; exists (\poly_(i < r.+1) f`_(i * p)). by apply: polyOver_poly => i _; rewrite (polyOverP _) ?minPolyOver. rewrite comp_polyE size_poly_eq -?Dn ?fn1 ?oner_eq0 //. have pr_p := charf_prime charLp; have p_gt0 := prime_gt0 pr_p. apply/polyP=> i; rewrite coef_sum. have [[{}i ->] | p'i] := altP (@dvdnP p i); last first. rewrite big1 => [|j _]; last first. rewrite coefZ -exprM coefXn [_ == _](contraNF _ p'i) ?mulr0 // => /eqP->. by rewrite dvdn_mulr. rewrite (dvdn_charf charLp) in p'i; apply: mulfI p'i _ _ _. by rewrite mulr0 mulr_natl; case: i => // i; rewrite -coef_deriv f'0 coef0. have [ltri | leir] := leqP r.+1 i. rewrite nth_default ?sz_f ?Dn ?ltn_pmul2r ?big1 // => j _. rewrite coefZ -exprM coefXn mulnC gtn_eqF ?mulr0 //. by rewrite ltn_pmul2l ?(leq_trans _ ltri). rewrite (bigD1 (Sub i _)) //= big1 ?addr0 => [|j i'j]; last first. by rewrite coefZ -exprM coefXn mulnC eqn_pmul2l // mulr_natr mulrb ifN_eqC. by rewrite coef_poly leir coefZ -exprM coefXn mulnC eqxx mulr1. 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)