proposition: Lemma poly_algR_pfactor (p : {poly algR}) : { r : seq algC | p ^^ algRval = val (lead_coef p) *: \prod_(z <- r) algCpfactor z }.
proof: Proof. wlog p_monic : p / p \is monic => [hwlog|]. have [->|pN0] := eqVneq p 0. by exists [::]; rewrite lead_coef0/= rmorph0 scale0r. have [|r] := hwlog ((lead_coef p)^-1 *: p). by rewrite monicE lead_coefZ mulVf ?lead_coef_eq0//. rewrite !lead_coefZ mulVf ?lead_coef_eq0//= scale1r. rewrite map_polyZ/= => /(canRL (scalerKV _))->; first by exists r. by rewrite fmorph_eq0 lead_coef_eq0. suff: {r : seq algC | p ^^ algRval = \prod_(z <- r) algCpfactor z}. by move=> [r rP]; exists r; rewrite rP (monicP _)// scale1r. have [/= r pr] := closed_field_poly_normal (p ^^ algRval). rewrite (monicP _) ?monic_map ?scale1r// {p_monic} in pr *. have [n] := ubnP (size r). elim: n r => // n IHn [|x r]/= in p pr *. by exists [::]; rewrite pr !big_nil. rewrite ltnS => r_lt. have xJxr : x^* \in x :: r. rewrite -root_prod_XsubC -pr. have /eq_map_poly-> : algRval =1 Num.conj_op \o algRval. by move=> a /=; rewrite (CrealP (algRvalP _)). by rewrite map_poly_comp mapf_root pr root_prod_XsubC mem_head. have xJr : (x \isn't Num.real) ==> (x^* \in r) by rewrite implyNb CrealE. have pxdvdC : algCpfactor x %| p ^^ algRval. rewrite pr algCpfactorE big_cons/= dvdp_mul2l ?polyXsubC_eq0//. by case: (_ \is _) xJr; rewrite ?dvd1p// dvdp_XsubCl root_prod_XsubC. pose pr'x := p %/ algRpfactor x. have [||r'] := IHn (if x \is Num.real then r else rem x^* r) pr'x; last 2 first. - by case: (_ \is _) in xJr *; rewrite ?size_rem// (leq_ltn_trans (leq_pred _)). - move=> /eqP; rewrite map_divp -dvdp_eq_mul ?algCpfactor_eq0//= => /eqP->. by exists (x :: r'); rewrite big_cons mulrC. rewrite map_divp/= pr big_cons algCpfactorE/=. rewrite divp_pmul2l ?expf_neq0 ?polyXsubC_eq0//. case: (_ \is _) => /= in xJr *; first by rewrite divp1//. by rewrite (big_rem _ xJr)/= mulKp ?polyXsubC_eq0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various)