Is there code for det

Stream: Is there code for X?

[Alex Kontorovich]

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]

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]

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]

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

[Eric Wieser]

@Yakov Pechersky and I worked on it very recently

[Eric Wieser]

#5593

[Eric Wieser]

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

[Yakov Pechersky]

@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