proposition: Lemma errloc_puncture (F : fieldType) n (f : 'rV[F]_n) (y : 'rV[F]_n) i : i \in supp y -> \sigma_(f, y) = (1 - f ``_ i *: 'X ) * \sigma_(f, y, i).
proof: Proof. move=> ?; rewrite {1}/errloc (bigD1 i) //=; congr (_ * _). by apply eq_bigl => j; rewrite in_setD1 andbC. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly) ssr_ext ssralg_ext cyclic_code dft