∀ {n : Type u_1} [inst : Fintype n] {A : Type u_4} (K : Type u_5) [inst_1 : DecidableEq n] [inst_2 : CommRing A]
  [Nontrivial A] [inst_4 : Field K] [inst_5 : Algebra A K] [IsFractionRing A K] {M : Matrix n n A},
  (∃ v, v ≠ 0 ∧ M.mulVec v = 0) ↔ M.det = 0