Definition matrix_mult {m n : nat} (mat1 : Matrix R m n) {p : nat} (mat2 : Matrix R n p) : (Matrix R m p) := λ i j, Σ ((row mat1 i) ^ (col mat2 j)).
Require Import UniMath.Foundations.PartA. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Combinatorics.FiniteSequences. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.IteratedBinaryOperations. Require Import UniMath.Algebra.RigsAndRings.