proposition: Lemma mulr_sum (R : ringType) m n (Fm : 'I_m -> R) (Fn : 'I_n -> R) : (\sum_(i < m) Fm i) * (\sum_(i < n) Fn i) = \sum_(i < m * n) ((Fm (mxtens_unindex i).1) * (Fn (mxtens_unindex i).2)).
proof: Proof. rewrite mulr_suml; transitivity (\sum_i (\sum_(j < n) Fm i * Fn j)). by apply: eq_big=> //= i _; rewrite -mulr_sumr. rewrite pair_big; apply: reindex=> //=. by exists mxtens_index=> i; rewrite (mxtens_indexK, mxtens_unindexK). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop ssralg matrix zmodp div)