Kirchoffs Matrix Tree Theorem for connected Simple Graphs

Stream: Is there code for X?

[Swarnava Chakraborty]

Thanks for this. Is there any thread or channel where someone tried to implement Kirchoffs Matrix Tree Theorem for connected Simple Graphs? @Eric Wieser

[Notification Bot]

A message was moved here from #Is there code for X? > Cauchy Binet theorem by Eric Wieser.

[Swarnava Chakraborty]

Hello, can anyone help me on how to proceed with the proof? Assume I have all the required lemmas defined and Cauchy-Binet theorem as well.

[Peter Nelson]

Can you provide a formal statement with a sorry, and also statements of what the required lemmas are, exactly? The devil tends to be in the details with these things.

[Peter Nelson]

The fact that every simple connected graph has a spanning tree (docs#SimpleGraph.Connected.exists_isTree_le) was only added to mathlib a couple of days ago.

[Swarnava Chakraborty]

Well the thing is, for proving it, I think I will need a bunch of lemmas , including results about minors of matrices (incidence matrix and laplacian matrix of a graph). I am stuck on how to define the minors. Could you help me out? @Peter Nelson

P.S. Sorry for the late reply.

[Peter Nelson]

For A : Matrix m n and s : Finset m and t : Finset n, you can define the minor with rows in s and columns in t by

example {m n R : Type*} (A : Matrix m n R) (s : Finset m) (t : Finset n) : Matrix s t R :=
  A.submatrix (fun x : s ↦ x.1) (fun x : t ↦ x.1)

There really is a lot of work to from here to get to the matrix tree theorem, though.