proposition: Lemma erreval_vecE i : i \in supp e -> e ``_ i * f ``_ i = - a ``_ i * \omega_(f, a, e).[(a ``_ i)^-1] / \sigma_(a, e)^`().[(a ``_ i)^-1].
proof: Proof. move=> iE. have morph_horner_add : {morph (fun x => x.[(a ``_ i)^-1]) : x y / x + y >-> x + y}. move=> x y; exact: hornerD. have morph_horner_mul : {morph (fun x => x.[(a ``_ i)^-1]) : x y / x * y >-> x * y}. move=> x y; exact: hornerM. have -> : \omega_(f, a, e).[(a ``_ i)^-1] = e ``_ i * f ``_ i * \prod_(j in supp e :\ i) (1 - a ``_ j * (a ``_ i)^-1). rewrite (@big_morph _ _ _ 0 _ _ _ morph_horner_add); last by rewrite horner0. rewrite [in LHS](big_setD1 i) //= [X in _ + X = _](_ :_ = 0); last first. rewrite (eq_bigr (fun=> 0)); first by rewrite big_const iter_addr0. move=> j Hj. rewrite !hornerE /= (@big_morph _ _ _ 1 _ _ _ morph_horner_mul); last by rewrite hornerE. rewrite (big_setD1 i) /=; last first. rewrite !inE eq_sym in Hj. rewrite !inE. case/andP : Hj => /= ->. by rewrite insupp in iE. by rewrite !hornerE /= divrr ?unitfE ?(proj2 Ha) // ?Ht' // subrr mulr0 mul0r. rewrite addr0 !hornerE /=; congr (_ * _). rewrite (@big_morph _ _ _ 1 _ _ _ morph_horner_mul); last by rewrite hornerE. apply eq_bigr => ? ?; by rewrite !hornerE. have -> : (\sigma_(a, e)^`()).[(a ``_ i)^-1] = - a ``_ i * \prod_(j in supp e :\ i) (1 - a ``_ j * (a ``_ i)^-1). rewrite derive_errloc (@big_morph _ _ _ 0 _ _ _ morph_horner_add); last by rewrite horner0. rewrite [in LHS](big_setD1 i) //= [X in _ + X = _](_ :_ = 0); last first. rewrite (eq_bigr (fun=> 0)); first by rewrite big_const iter_addr0. move=> j Hj. rewrite !hornerE /= (@big_morph _ _ _ 1 _ _ _ morph_horner_mul); last by rewrite hornerE. rewrite (big_setD1 i) /=; last first. rewrite !inE; move: Hj. rewrite !inE eq_sym => /andP[-> /=]. by rewrite insupp in iE. by rewrite !hornerE /= divrr ?unitfE ?(proj2 Ha) // ?Ht' // subrr mulr0 mul0r. rewrite addr0 !hornerE /=; congr (_ * _). rewrite (@big_morph _ _ _ 1 _ _ _ morph_horner_mul); last by rewrite hornerE. apply eq_bigr => ? ?; by rewrite !hornerE. rewrite mulrCA mulrK // unitrM unitrN unitfE (proj2 Ha) /=. apply big_ind. - by rewrite unitr1. - by move=> x y; rewrite unitrM => -> ->. - move=> j Hj; rewrite GRing.unitfE. suff : a ``_ j / a ``_ i != 1. by apply: contra => /eqP /(congr1 (fun x => x + a ``_ j / a ``_ i)); rewrite subrK add0r => <-. apply/eqP => /(congr1 (fun x => x * a ``_ i)). rewrite -mulrA mulVr ?unitfE ?(proj2 Ha) ?expf_neq0 // mulr1 mul1r. move: (proj1 Ha) => /(_ j i); rewrite 2!ffunE => aij. move/aij => ij; subst j. move: Hj; by rewrite in_setD1 eqxx. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly) ssr_ext ssralg_ext cyclic_code dft