{R : Ring@{i}} {m n k : nat} (M : Matrix R m n) (N : Matrix R n k) : Matrix R m k. Proof. snrapply Build_Matrix. intros i j Hi Hj. exact (ab_sum n (fun k Hk => entry M i k * entry N k j)). Defined.
Require Import Basics.Overture Basics.Trunc Basics.Tactics Basics.Decidable. Require Import Types.Sigma. Require Import Spaces.List.Core Spaces.List.Theory Spaces.List.Paths. Require Import Algebra.Rings.Ring Algebra.Rings.Module Algebra.Rings.CRing Require Import abstract_algebra. Require Import WildCat.Core WildCat.Paths. Require Import Modalities.ReflectiveSubuniverse.