proposition: Lemma mmap1_eq n (R : ringType) (f1 f2 : 'I_n -> R) m : f1 =1 f2 -> mmap1 f1 m = mmap1 f2 m.
proof: Proof. move=> eq_f; rewrite /mmap1; apply/eq_bigr. by move=> /= i _; rewrite eq_f. 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