Stream: Is there code for X?
Topic: Is there code for det
Alex Kontorovich (Jan 09 2021 at 18:03):
Hello! I see that matrix.det is defined as a sum over equiv.perm's etc. Is there code for evaluating det as an alternating sum with minors? (Then it would be easy to, say, get a 2x2 det explicitly as ad-bc, etc) Thanks!
Adam Topaz (Jan 09 2021 at 18:11):
Unfortunately, the word
minor doesn't appear in the
linear_algbera.determinant file. My guess is that this doesn't exist in mathlib, but I would be happy to be wrong.
Sebastien Gouezel (Jan 09 2021 at 18:19):
There are a lot of minors in
nonsingular_inverse.lean (see docs#matrix.adjugate for instance), but probably not the specific formula you are looking for.
Eric Wieser (Jan 09 2021 at 18:19):
There is a PR today to get
ad - bc via simp
Eric Wieser (Jan 09 2021 at 18:20):
@Yakov Pechersky and I worked on it very recently
Eric Wieser (Jan 09 2021 at 18:22):
Eric Wieser (Jan 09 2021 at 18:23):
That ought to give the pieces needed to write a lemma about minors
Yakov Pechersky (Jan 09 2021 at 23:44):
@Alex Kontorovich I also have a local branch defining det using the Laplace expansion which is exactly about minors. The PR Eric mentioned might help in proving the two definitions as interchangeable
Last updated: May 17 2021 at 16:26 UTC