proposition: Lemma size_errloc_eq a E : distinct_non_zero a -> size (errloc a E) = #| E |.+1.
proof: Proof. move=> Ha. rewrite /errloc. rewrite (eq_bigr (fun i : 'I_n => (- a ``_ i *: ('X - (a ``_ i)^-1%:P)))); last first. move=> i iE. rewrite scalerDr addrC !scaleNr scalerN opprK; congr (_ + _). rewrite -mul_polyC -!alg_polyC mulr_algl scalerA. rewrite divrr // ?alg_polyC // unitfE. by case: Ha => _; apply. rewrite scaler_prod size_scale; last first. apply/prodf_neq0 => i iE; by rewrite oppr_eq0 (proj2 Ha). rewrite (_ : \prod_(i in E) ('X - (a ``_ i)^-1%:P) = \prod_(i <- enum E) ('X - (a ``_ i)^-1%:P)); last by rewrite big_filter. by rewrite size_prod_XsubC cardE. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly) ssr_ext ssralg_ext cyclic_code dft