no goals
R : Type ?u.531459
M✝ : Type ?u.531462
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M✝
inst✝⁴ : Module R M✝
n : Type u_2
inst✝³ : Fintype n
A : Type u_1
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
⊢ (∃ v x, vecMul v M = 0) ↔ det M = 0
simpa only [← M.det_transpose, ← mulVec_transpose] using exists_mulVec_eq_zero_iff