proposition: Lemma swapXY_map (R S : ringType) (f : {additive R -> S}) u : swapXY (u ^ map_poly f) = swapXY u ^ map_poly f.
proof: Proof. by apply/polyP=> i; apply/polyP=> j; rewrite !(coef_map, coef_swapXY). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice ssrnat seq) mathcomp(fintype tuple finfun bigop fingroup perm div) mathcomp(ssralg zmodp matrix mxalgebra) mathcomp(poly polydiv mxpoly binomial)