Commit 2023-11-14 18:47 e004ac1c

View on Github →

feat: add 2-coloring of pathGraph and prove its chromatic number is 2 (#8166) Define a bicoloring for pathGraph and prove that when 2 ≤ n its chromatic number is 2. Creates a ConcreteColorings module to hold such colorings of concrete graphs.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean

added theorem SimpleGraph.chromaticNumber_pathGraph

added def SimpleGraph.pathGraph.bicoloring

added def SimpleGraph.pathGraph_two_embedding

Modified Mathlib/Combinatorics/SimpleGraph/Hasse.lean

added theorem SimpleGraph.pathGraph_adj

added theorem SimpleGraph.pathGraph_two_eq_top

Modified Mathlib/Data/Nat/Parity.lean

added theorem Nat.succ_mod_two_eq_one_iff

added theorem Nat.succ_mod_two_eq_zero_iff