proposition: Lemma derive_errloc (a : 'rV[F]_n) E : (errloc a E)^`() = \sum_(j in E) - a ``_ j *: \prod_(k in E :\ j) (1 - a ``_ k *: 'X).
proof: Proof. move Hm : (#| E |) => m. elim: m E Hm => [E /eqP| m IH E Em]. rewrite cards_eq0 => /eqP ->; by rewrite /errloc 2!big_set0 derivC. have [/= f Hf] : exists f, f \in E by apply/set0Pn; rewrite -cards_eq0 Em. rewrite /errloc (big_setD1 f) //= derivM IH; last first. move: (cardsD1 f E); rewrite Hf /= add1n Em; by case. rewrite derivB derivC sub0r linearZ /= derivX. rewrite [in RHS](big_setD1 f) //=; congr (_ + _). by rewrite alg_polyC -mul_polyC polyCN. rewrite big_distrr /=; apply eq_bigr => i Hi. rewrite mulrC -!mul_polyC -mulrA; congr (_ * _). rewrite [in RHS](big_setD1 f) //=; last first. rewrite in_setD1; by move: Hi; rewrite in_setD1 eq_sym => /andP [] ->. rewrite mulrC mul_polyC; congr (_ * _). apply eq_bigl => ?; rewrite !in_setD1; bool_congr. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly) ssr_ext ssralg_ext cyclic_code dft