proposition: Lemma horner_mx_diag (d : 'rV[R]_n) (p : {poly R}) : horner_mx (diag_mx d) p = diag_mx (map_mx (horner p) d).
proof: Proof. apply/matrixP => i j; rewrite !mxE. elim/poly_ind: p => [|p c ihp]; first by rewrite rmorph0 horner0 mxE mul0rn. rewrite !hornerE mulrnDl rmorphD rmorphM /= horner_mx_X horner_mx_C !mxE. rewrite (bigD1 j)//= ihp mxE ?eqxx mulr1n -mulrnAl big1 ?addr0//. by case: (altP (i =P j)) => [->|]; rewrite /= !(mulr1n, addr0, mul0r). by move=> k /negPf nkF; rewrite mxE nkF mulr0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)