Definition entrywise {X : UU} (n m : nat) (op : binop X) : binop (Matrix X n m) := λ mat1 mat2 i, pointwise _ op (mat1 i) (mat2 i).
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.