proposition: Lemma commr_mmap_is_multiplicative: multiplicative (mmap f h).
proof: Proof. split=> //= [p q|]; last first. by rewrite /mmap msupp1 big_seq1 mpolyCK rmorph1 mul1r mmap11. pose_big_enough i. rewrite (mpolywME (k := i)) // raddf_sum /= !(mmapE i) //. rewrite big_distrlr /= pair_bigA; apply/eq_bigr=> /=. case=> j1 j2 _ /=; rewrite mmapZ mmapX; apply/esym. rewrite [f q@__ * _]commr_f mulrA -[X in X*_]mulrA. by rewrite -commr_mmap1_M // -mulrA -commr_f !mulrA rmorphM. by close. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg