fact: Definition coweighting {m n : nat} (mat : Matrix R m n) : UU := ∑ vec : Vector R m, ((row_vec vec) ** mat) = row_vec (const_vec (1%rig)).
imports: UniMath.Foundations.PartA UniMath.MoreFoundations.PartA UniMath.Combinatorics.FiniteSequences UniMath.Algebra.BinaryOperations UniMath.Algebra.IteratedBinaryOperations UniMath.Algebra.RigsAndRings