proposition: Lemma decomp_errloc (a :'rV[F]_n) E : (forall i, a ``_ i != 0) -> errloc a E = (\prod_(i in E) (- a ``_ i)%:P) * \prod_(i in E) ('X - (a ``_ i)^-1%:P).
proof: Proof. move=> a0. rewrite /errloc (eq_bigr (fun i : 'I_n => (- a ``_ i)%:P * ('X - (a ``_ i)^-1%:P))). by rewrite big_split. move=> i iE. rewrite -polyCN mulrDr -polyCM mulrNN divff //. by rewrite polyC1 -(addrC 1) polyCN mulNr mul_polyC. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly) ssr_ext ssralg_ext cyclic_code dft