proposition: Lemma Primitive_Element_Theorem : exists z, (<< <<K; y>>; x>> = <<K; z>>)%VS.
proof: Proof. have /polyOver_subvs[p Dp]: minPoly K x \is a polyOver K := minPolyOver K x. have nz_pKx: minPoly K x != 0 by rewrite monic_neq0 ?monic_minPoly. have{nz_pKx} nz_p: p != 0 by rewrite Dp map_poly_eq0 in nz_pKx. have{Dp} px0: root (map_poly vsval p) x by rewrite -Dp root_minPoly. have [q0 [Kq0 q0y0 sepKq0]] := separable_elementP sepKy. have /polyOver_subvs[q Dq]: minPoly K y \is a polyOver K := minPolyOver K y. have qy0: root (map_poly vsval q) y by rewrite -Dq root_minPoly. have sep_pKy: separable_poly (minPoly K y). by rewrite (dvdp_separable _ sepKq0) ?minPoly_dvdp. have{sep_pKy} sep_q: separable_poly q by rewrite Dq separable_map in sep_pKy. have [r nz_r PETr] := large_field_PET nz_p px0 qy0 sep_q. have [[s [Us Ks /ltnW leNs]] | //] := finite_PET (size r). have{s Us leNs} /allPn[t {}/Ks Kt nz_rt]: ~~ all (root r) s. by apply: contraTN leNs; rewrite -ltnNge => /max_poly_roots->. have{PETr} [/= [p1 Dx] [q1 Dy]] := PETr (Subvs Kt) nz_rt. set z := t * y - x in Dx Dy; exists z; apply/eqP. rewrite eqEsubv !(sameP FadjoinP andP) subv_adjoin. have Kz_p1z (r1 : {poly subvs_of K}): (map_poly vsval r1).[z] \in <<K; z>>%VS. rewrite rpred_horner ?memv_adjoin ?(polyOverSv (subv_adjoin K z)) //. by apply/polyOver_subvs; exists r1. rewrite -{1}Dx -{1}Dy !{Dx Dy}Kz_p1z /=. rewrite (subv_trans (subv_adjoin K y)) ?subv_adjoin // rpredB ?memv_adjoin //. by rewrite subvP_adjoin // rpredM ?memv_adjoin ?subvP_adjoin. 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)