Chromatic number
Lax825442.ChromaticNumber · concepts/Lax825442/ChromaticNumber.lean · lax-825442
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
The chromatic number is the minimum number of colors in a proper vertex coloring. This interface takes the natural part of mathlib’s chromatic number, which is finite on finite graphs. Mathlib's gives a coloring with at most the number of vertices, so conversion to a natural number loses no information.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Chromatic number |
| 6 | type: definition |
| 7 | --- |
| 8 | The chromatic number is the minimum number of colors in a proper vertex |
| 9 | coloring. This interface takes the natural part of mathlib’s chromatic number, |
| 10 | which is finite on finite graphs. |
| 11 | Mathlib's `SimpleGraph.colorable_of_fintype` gives a coloring with at most |
| 12 | the number of vertices, so conversion to a natural number loses no information. |
| 13 | -/ |
| 14 | |
| 15 | namespace Lax825442.ChromaticNumber |
| 16 | |
| 17 | /-- The natural-valued chromatic number of a finite graph. -/ |
| 18 | noncomputable def chromaticNumber {V : Type} [Fintype V] [DecidableEq V] |
| 19 | (G : SimpleGraph V) : ℕ := |
| 20 | G.chromaticNumber.toNat |
| 21 | |
| 22 | end Lax825442.ChromaticNumber |
| 23 | |
| 24 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments