∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonAssocSemiring α] [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  {M N : Matrix m n α}, (∀ (i : n), M.mulVec (Pi.single i 1) = N.mulVec (Pi.single i 1)) → M = N