Commit 2024-01-15 11:29 59641348
View on Github →refactor: make SimpleGraph.chromaticNumber be ENat-valued (#8883)
This removes an awkwardness of the API, where theorems had to include colorability hypotheses. This trades that awkwardness for a smaller one, which is that one writes G.Colorable (ENat.toNat G.chromaticNumber) rather than G.Colorable G.chromaticNumber.
It would be good to have a followup refactoring PR to more carefully evaluate the API after this change.