non-trivial kernel iff determinant zero

Stream: maths

[Apurva Nakade]

Oops, I just realized I posted the converse of what I actually wanted

import linear_algebra.matrix
import linear_algebra.nonsingular_inverse
open matrix
open_locale classical
example {k n : Type u}
  [field k]
  [fintype n]
  (M : matrix n n k) :
  M.det = 0 →
    ∃ v : n → k, v ≠ 0 ∧ M.mul_vec v = 0 :=
begin
  sorry,
end

[Apurva Nakade]

I managed to get the other direction in a roundabout way using the inverse of M but in this direction I am not able to see what to use.

[Aaron Anderson]

We’ve proven that an injective linear map has an inverse, so you could use that for the contrapositive

[Aaron Anderson]

Or any column vector of the adjugate should be in the kernel

[Apurva Nakade]

This is very interesting. I have never worked with the adjoint matrix in the non-invertible case.

[Apurva Nakade]

Thanks again. Found the exact statement that I need lemma mul_adjugate (A : matrix n n α) : A ⬝ adjugate A = A.det • 1