Revision #1275 → #1763 · back to history
modifiedGraph4f2378b011ef
| Field | From #1275 | To #1763 |
|---|
| mathlib.match_kind | — | exact |
| note | Undirected graphs are formalized as SimpleGraph (simple) and Graph (general multigraph in Mathlib.Combinatorics.Graph.Basic). | Undirected simple graphs are formalized as SimpleGraph; general multigraphs as Graph in Mathlib.Combinatorics.Graph.Basic. |
modifiedDirected graph7f720204ad7d
| Field | From #1275 | To #1763 |
|---|
| note | Quiver formalizes directed graphs (as a directed multigraph, generalizing simple digraphs). | Quiver formalizes directed (multi)graphs, generalizing simple digraphs. |
modifiedMultigraph130fe0299f11
| Field | From #1275 | To #1763 |
|---|
| note | Graph α β models multigraphs with vertex/edge sets and incidence data allowing parallel edges and loops. | Graph α β models multigraphs with parallel edges and loops via incidence data. |
addedSeven Bridges of Königsberg7c85f097c531
addedEuler's polyhedron formula5812ff771c1d
modifiedGraph coloring4643bb1fdce2
| Field | From #1275 | To #1763 |
|---|
| mathlib.module | Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring | Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex |
| note | Proper vertex colorings are formalized as SimpleGraph.Coloring with Colorable and chromaticNumber. | Proper vertex colorings are formalized as SimpleGraph.Coloring with associated Colorable and chromaticNumber. |
modifiedFour-color theoremc71be2aa0255
| Field | From #1275 | To #1763 |
|---|
| note | The four-color theorem is not formalized in Mathlib (it requires planarity). | The four-color theorem is not formalized in Mathlib (no planarity). |
addedFive-color theorem9610fb590b56
modifiedSpectral graph theory51b6f2ea6871
| Field | From #1275 | To #1763 |
|---|
| note | Adjacency/Laplacian matrices and some spectral results (positive semidefiniteness, connected-component kernel dimension) are formalized, but not a general spectral theory. | Adjacency/Laplacian matrices and some spectral results exist, but not a general spectral theory. |
modifiedTutte polynomial0ae150459db7
| Field | From #1275 | To #1763 |
|---|
| note | The Tutte polynomial is absent (the file Tutte.lean concerns Tutte's matching theorem, not the polynomial). | The Tutte polynomial is absent from Mathlib (the existing Tutte material concerns Tutte's matching theorem). |
addedHadwiger–Nelson problema31d1bf42e3a
modifiedUnit disk graph80e97e4010ec
| Field | From #1275 | To #1763 |
|---|
| note | Unit disk graphs are not defined (Mathlib's UnitDistance graphs are a different family). | Unit disk graphs are not defined in Mathlib (UnitDistance graphs are a different family). |
modifiedTurán's theorem3ec185ee2226
| Field | From #1275 | To #1763 |
|---|
| note | Turán's theorem is formalized in full as an isomorphism characterization of extremal Kr+1-free graphs. | Turán's theorem is formalized as an isomorphism characterization of extremal Kr+1-free graphs. |
addedGraph homomorphism18a894b8538a
modifiedSzemerédi's regularity lemma9d1ddc4ac479
| Field | From #1275 | To #1763 |
|---|
| mathlib.decl | SimpleGraph.szemeredi_regularity | szemeredi_regularity |
| note | Szemerédi's regularity lemma is formalized as szemeredi_regularity giving an ε-uniform equipartition. | Szemerédi's regularity lemma is formalized as szemeredi_regularity giving an ε-uniform equipartition of bounded size. |
modifiedUniform spanning tree3ba17df2bb3a
| Field | From #1275 | To #1763 |
|---|
| note | Uniform spanning trees (and spanning trees as a counted object) are not formalized in Mathlib. | Uniform spanning trees are not formalized in Mathlib. |
modifiedLaplacian matrix2ef0353d06c3
| Field | From #1275 | To #1763 |
|---|
| note | The Laplacian is formalized as SimpleGraph.lapMatrix = degMatrix - adjMatrix. | The Laplacian is formalized as SimpleGraph.lapMatrix = degMatrix − adjMatrix. |
addedErdős–Faber–Lovász conjectureabfdeb227da2
addedTotal coloring conjecture8b59c6408b49
addedList coloring conjecture8d2bac80a2b6
addedHadwiger conjectured7f15473e2b6
addedHamiltonian path problemd2c6cfd91cc2
addedMinimum spanning treeb3b92a03926d
addedShortest path problem453bff27f150
addedTraveling salesman problemdb95911c732c