proposition: Lemma map_horner_mx p : (horner_mx A p)^f = horner_mx A^f (fp p).
proof: Proof. rewrite -[p](poly_rV_K (leqnn _)) map_rVpoly. by rewrite !horner_rVpoly map_vec_mx map_mxM map_powers_mx. 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)