Revision #2284 → #2935 · back to history
modifiedDirected graph7f720204ad7d
| Field | From #2284 | To #2935 |
|---|
| mathlib.decl | Quiver | Digraph |
| mathlib.match_kind | generalization | exact |
| mathlib.module | Mathlib.Combinatorics.Quiver.Basic | Mathlib.Combinatorics.Digraph.Basic |
| note | Quiver formalizes directed (multi)graphs, generalizing simple digraphs. | Directed graphs are formalized directly as Digraph (structurally equivalent to Quiver.{0}) in Mathlib.Combinatorics.Digraph.Basic. |
addedErdős–Rényi model1ed7ca2c5836
addedDirected acyclic graph19ca7e2cbc2b
modifiedHamiltonian path problemd2c6cfd91cc2
| Field | From #2284 | To #2935 |
|---|
| mathlib.decl | — | SimpleGraph.IsHamiltonian |
| mathlib.module | — | Mathlib.Combinatorics.SimpleGraph.Hamiltonian |
| note | Hamiltonian paths/cycles and the decision problem are not formalized in Mathlib. | Hamiltonian walks (SimpleGraph.Walk.IsHamiltonian) and Hamiltonian graphs (SimpleGraph.IsHamiltonian) are defined, but the computational decision problem is not addressed. |
| status | not_formalized | partial |
addedRoute inspection problem339ce7f97145
addedSteiner tree problem77653aeb36ea