proposition: Lemma closed_field_poly_normal p : {r : seq F | p = lead_coef p *: \prod_(z <- r) ('X - z%:P)}.
proof: Proof. apply: sig_eqW; have [r [q [->]]] /= := dec_factor_theorem p. have [->|] := eqVneq; first by exists [::]; rewrite mul0r lead_coef0 scale0r. have [[x rqx ? /(_ isT x) /negP /(_ rqx)] //|] := altP (closed_rootP q). rewrite negbK => /size_poly1P [c c_neq0-> _ _]; exists r. rewrite mul_polyC lead_coefZ (monicP _) ?mulr1 //. by rewrite monic_prod => // i; rewrite monicXsubC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)