Commit 2025-09-17 01:02 fff031ec

View on Github →

feat(SimpleGraph): remove finiteness assumption from isEmpty_of_chromaticNumber_eq_zero (#29578)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Coloring.lean

added theorem SimpleGraph.chromaticNumber_eq_zero_of_isEmpty

deleted theorem SimpleGraph.chromaticNumber_eq_zero_of_isempty

modified theorem SimpleGraph.isEmpty_of_chromaticNumber_eq_zero