Zulip Chat Archive

Stream: maths

Topic: non-trivial kernel implies determinant zero


view this post on Zulip Apurva Nakade (Aug 14 2020 at 00:45):

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,

view this post on Zulip Alex J. Best (Aug 14 2020 at 00:51):

Please include the imports and stuff like

import linear_algebra.matrix
open matrix
open_locale classical

too!

view this post on Zulip Aaron Anderson (Aug 14 2020 at 00:56):

Check linear_algebra/nonsingular_inverse

view this post on Zulip Aaron Anderson (Aug 14 2020 at 00:57):

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

view this post on Zulip Apurva Nakade (Aug 14 2020 at 00:58):

Ah! thanks! And sorry about the imports


Last updated: May 10 2021 at 07:15 UTC