∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Fintype n] [inst_1 : Fintype m] [inst_2 : Field R]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] (A : Matrix m n R), (A.transpose * A).rank = A.rank