proposition: Lemma adjoin_separableP {K x} : reflect (forall y, y \in <<K; x>>%VS -> separable_element K y) (separable_element K x).
proof: Proof. apply: (iffP idP) => [sepKx | -> //]; last exact: memv_adjoin. move=> _ /Fadjoin_polyP[q Kq ->]; apply/Derivation_separableP=> D derD DK_0. apply/subvP=> _ /Fadjoin_polyP[p Kp ->]. rewrite memv_ker -(extendDerivation_id x D (mempx_Fadjoin _ Kp)). have sepFyx: (separable_element <<K; q.[x]>> x). by apply: (separable_elementS (subv_adjoin _ _)). have KyxEqKx: (<< <<K; q.[x]>>; x>> = <<K; x>>)%VS. apply/eqP; rewrite eqEsubv andbC adjoinSl ?subv_adjoin //=. apply/FadjoinP/andP; rewrite memv_adjoin andbT. by apply/FadjoinP/andP; rewrite subv_adjoin mempx_Fadjoin. have /[!KyxEqKx] derDx := extendDerivationP derD sepFyx. rewrite -horner_comp (Derivation_horner derDx) ?memv_adjoin //; last first. by apply: (polyOverSv (subv_adjoin _ _)); apply: polyOver_comp. set Dx_p := map_poly _; have Dx_p_0 t: t \is a polyOver K -> (Dx_p t).[x] = 0. move/polyOverP=> Kt; congr (_.[x] = 0): (horner0 x); apply/esym/polyP => i. have /eqP Dti_0: D t`_i == 0 by rewrite -memv_ker (subvP DK_0) ?Kt. by rewrite coef0 coef_map /= {1}extendDerivation_id ?subvP_adjoin. rewrite (Derivation_separable derDx sepKx) -/Dx_p Dx_p_0 ?polyOver_comp //. by rewrite add0r mulrCA Dx_p_0 ?minPolyOver ?oppr0 ?mul0r. 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)