proposition: Lemma commr_mmap_is_multiplicative: multiplicative (mmap f h).
proof: Proof. split => [g1 g2|]; last by rewrite mmap1. rewrite malgME raddf_sum mulr_suml /=; apply: eq_bigr=> i _. rewrite raddf_sum mulr_sumr /=; apply: eq_bigr=> j _. by rewrite mmapU /= rmorphM mmorphM -mulrA [X in _*X=_]mulrA commr_f !mulrA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap