proposition: Lemma lead_coef_prod {R : idomainType} (ps : seq {poly R}) : lead_coef (\prod_(p <- ps) p) = \prod_(p <- ps) lead_coef p.
proof: Proof. by apply/big_morph/lead_coef1; apply: lead_coefM. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)