lean-graph-matrices

Formalize a statement and proof of the matrix tree theorem in Lean:

If $G$ is a simple graph with Laplacian matrix $L$, then for any vertex $q$ we have $\qquad \det L |_q = \#(\text{spanning trees of }G)$,
where $L |_q$ denotes the matrix with $q$-indexed row and column removed.

Pieces of theorem statement

• Laplacian matrix, mathlib: SimpleGraph.lapMatrix
• subgraph, mathlib: SimpleGraph.Subgraph
  • spanning tree, mathlib: SimpleGraph.IsTree
• determinant, mathlib: Matrix.det
• submatrix, mathlib: Matrix.submatrix
  • subsets, mathlib: Finset.powersetCard
  • inclusion maps, mathlib: OrderEmbedding

Other references:

• Formalization of the Königsberg bridges problem by Kyle Miller, on working with an explicit graph

• SimpleGraph.fromEdgeSet, define a graph from its edge set

• Finset.erase, erase an element from a finite set

• SimpleGraph.incMatrix, the unsigned incidence matrix of a graph

• Finset.sum_const_nat

• Fin.sum_const

• monoEquivOfFin, order isomorphism between V and Fin (card V)

• Finset.orderEmbOfFin, increasing bijection between Fin (card V) and V

• Matrix.reindex

Using Lean

Search tools:

• human language
  • Lean search
  • Zulip chat
  • Moogle
• Lean code
  • Loogle