proposition: Lemma minPoly_decidable_closure (F : fieldType) (L : closedFieldType) (FtoL : {rmorphism F -> L}) x : decidable_embedding FtoL -> integralOver FtoL x -> {p | [/\ p \is monic, root (p ^ FtoL) x & irreducible_poly p]}.
proof: Proof. move=> isF /sig2W[p /monicP mon_p px0]. have [r Dp] := closed_field_poly_normal (p ^ FtoL); pose n := size r. rewrite lead_coef_map {}mon_p rmorph1 scale1r in Dp. pose Fpx q := (q \is a polyOver isF) && root q x. have FpxF q: Fpx (q ^ FtoL) = root (q ^ FtoL) x. by rewrite /Fpx polyOver_poly // => j _; apply/sumboolP; exists q`_j. pose p_ (I : {set 'I_n}) := \prod_(i <- enum I) ('X - (r`_i)%:P). have{px0 Dp} /ex_minset[I /minsetP[/andP[FpI pIx0] minI]]: exists I, Fpx (p_ I). exists setT; suffices ->: p_ setT = p ^ FtoL by rewrite FpxF. by rewrite Dp (big_nth 0) big_mkord /p_ big_enum; apply/eq_bigl => i /[1!inE]. have{p} [p DpI]: {p | p_ I = p ^ FtoL}. exists (p_ I ^ (fun y => if isF y is left Fy then sval (sig_eqW Fy) else 0)). rewrite -map_poly_comp map_poly_id // => y /(allP FpI) /=. by rewrite unfold_in; case: (isF y) => // Fy _; case: (sig_eqW _). have mon_pI: p_ I \is monic by apply: monic_prod_XsubC. have mon_p: p \is monic by rewrite -(map_monic FtoL) -DpI. exists p; rewrite -DpI; split=> //; split=> [|q nCq q_dv_p]. by rewrite -(size_map_poly FtoL) -DpI (root_size_gt1 _ pIx0) ?monic_neq0. rewrite -dvdp_size_eqp //; apply/eqP. without loss mon_q: q nCq q_dv_p / q \is monic. move=> IHq; pose a := lead_coef q; pose q1 := a^-1 *: q. have nz_a: a != 0 by rewrite lead_coef_eq0 (dvdpN0 q_dv_p) ?monic_neq0. have /IHq IHq1: q1 \is monic by rewrite monicE lead_coefZ mulVf. by rewrite -IHq1 ?size_scale ?dvdpZl ?invr_eq0. without loss{nCq} qx0: q mon_q q_dv_p / root (q ^ FtoL) x. have /dvdpP[q1 Dp] := q_dv_p; rewrite DpI Dp rmorphM rootM -implyNb in pIx0. have mon_q1: q1 \is monic by rewrite Dp monicMr in mon_p. move=> IH; apply: (IH) (implyP pIx0 _) => //; apply: contra nCq => /IH IHq1. rewrite natr1E -(subnn (size q1)) {1}IHq1 ?Dp ?dvdp_mulr //. rewrite polySpred ?monic_neq0 //. by rewrite eqSS size_monicM ?monic_neq0 // -!subn1 subnAC addKn. have /dvdp_prod_XsubC[m Dq]: q ^ FtoL %| p_ I by rewrite DpI dvdp_map. pose B := [set j in mask m (enum I)]; have{} Dq: q ^ FtoL = p_ B. apply/eqP; rewrite -eqp_monic ?monic_map ?monic_prod_XsubC //. congr (_ %= _): Dq; apply: perm_big => //. by rewrite uniq_perm ?mask_uniq ?enum_uniq // => j; rewrite mem_enum inE. rewrite -!(size_map_poly FtoL) Dq -DpI (minI B) // -?Dq ?FpxF //. by apply/subsetP=> j /[1!inE] /mem_mask; rewrite mem_enum. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq choice) mathcomp(div fintype path tuple bigop finset prime order) mathcomp(ssralg poly polydiv mxpoly countalg closed_field) mathcomp(ssrnum ssrint archimedean rat intdiv fingroup) mathcomp(finalg zmodp cyclic pgroup sylow vector falgebra) mathcomp(fieldext separable galois)