proposition: Lemma map_mxT A B : (A *t B)^f = A^f *t B^f :> 'M_(m*p, n*q).
proof: Proof. by apply/matrixP=> i j; rewrite !mxE /= rmorphM. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop ssralg matrix zmodp div)