Zulip Chat Archive

Stream: Is there code for X?

Topic: Is there code for det


view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Jan 09 2021 at 18:19):

There is a PR today to get ad - bc via simp

view this post on Zulip Eric Wieser (Jan 09 2021 at 18:20):

@Yakov Pechersky and I worked on it very recently

view this post on Zulip Eric Wieser (Jan 09 2021 at 18:22):

#5593

view this post on Zulip Eric Wieser (Jan 09 2021 at 18:23):

That ought to give the pieces needed to write a lemma about minors

view this post on Zulip 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