## Stream: maths

### Topic: non-trivial kernel iff determinant zero

#### 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


#### 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.

#### 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

#### Aaron Anderson (Aug 14 2020 at 04:44):

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

#### 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.

#### 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