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