fact: Definition magnitude {n m : nat} (m : Matrix R m n) (has : has_magnitude m) : R := Σ (pr1 (dirprod_pr1 has)).
imports: UniMath.Foundations.PartA UniMath.MoreFoundations.PartA UniMath.Combinatorics.FiniteSequences UniMath.Algebra.BinaryOperations UniMath.Algebra.IteratedBinaryOperations UniMath.Algebra.RigsAndRings