Commit 2025-01-22 10:18 95dba76c

View on Github →

feat(Combinatorics/SimpleGraph): chromatic number of cycle graph (#20117)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Circulant.lean

added def SimpleGraph.cycleGraph_EulerianCircuit

added theorem SimpleGraph.cycleGraph_EulerianCircuit_length

Modified Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean

added theorem SimpleGraph.chromaticNumber_cycleGraph_of_even

added theorem SimpleGraph.chromaticNumber_cycleGraph_of_odd

added def SimpleGraph.cycleGraph.bicoloring_of_even

added def SimpleGraph.cycleGraph.tricoloring