proposition: Lemma errloc_zero (a : 'rV[F]_n) E (i : 'I_n) : distinct_non_zero a -> ((errloc a E).[(a ``_ i)^-1] == 0) = (i \in E).
proof: Proof. move=> Ha; apply/idP/idP => H. - apply/negPn/negP => abs; move/eqP: H. apply/rootP. rewrite (decomp_errloc _ (proj2 Ha)) ?unitfE //= rootM negb_or. apply/andP; split. rewrite -(@big_morph _ _ _ _ _ 1 _ (@polyCM F)) // rootC prodf_seq_neq0 /=. apply/allP => n0 _. apply/implyP => _; by rewrite oppr_eq0 (proj2 Ha). move: (root_prod_XsubC [seq (a ``_ x)^-1 | x : 'I_n <- enum E] (a ``_ i)^-1). rewrite big_map -[in X in _ -> X]big_filter => ->. apply: contra abs. case/mapP => /= j Hj /invr_inj aij. move: (proj1 Ha) => /(_ i j); rewrite 2!ffunE => /(_ aij) ->. by rewrite -mem_enum. - rewrite /errloc horner_prod prodf_seq_eq0. apply/hasP; exists i => //. rewrite H /= !hornerE divff ?(proj2 Ha) ?subrr // expf_neq0. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly) ssr_ext ssralg_ext cyclic_code dft