non-trivial kernel implies determinant zero

Stream: maths

[Apurva Nakade]

Is there a quick way to finish this:

example {k n : Type u}
  [field k]
  [fintype n]
  {M : matrix n n k}
  (v : n → k)
  (hv_ne0 : v ≠ 0)
  (hv_ker : M.mul_vec v = 0) :
  M.det = 0 :=
begin
  sorry,
end

I could not find anything on mathlib_docs and library_search also returned nothing.
Thanks,

[Alex J. Best]

Please include the imports and stuff like

import linear_algebra.matrix
open matrix
open_locale classical

too!

[Aaron Anderson]

Check linear_algebra/nonsingular_inverse

[Aaron Anderson]

We have that a matrix is a unit iff its determinant is. That should get you close enough

[Apurva Nakade]

Ah! thanks! And sorry about the imports