Zulip Chat Archive

Stream: maths

Topic: non-trivial kernel iff determinant zero


view this post on Zulip Apurva Nakade (Aug 14 2020 at 03:48):

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

view this post on Zulip Apurva Nakade (Aug 14 2020 at 03:51):

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.

view this post on Zulip Aaron Anderson (Aug 14 2020 at 04:43):

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

view this post on Zulip Aaron Anderson (Aug 14 2020 at 04:44):

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

view this post on Zulip Apurva Nakade (Aug 14 2020 at 05:48):

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

view this post on Zulip Apurva Nakade (Aug 14 2020 at 05:50):

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


Last updated: May 18 2021 at 07:19 UTC