Commit 2026-05-23 01:27 d8de6b61

View on Github →

feat(Combinatorics/SimpleGraph/Coloring/VertexColoring): chromaticNumber ⊤ and other small lemmas (#38424)

  • Golf isEmpty_of_colorable_zero and rename to Colorable.isEmpty
  • colorable_one_iff: G.Colorable 1 ↔ G = ⊥
  • Combine chromaticNumber_eq_zero_of_isEmpty/isEmpty_of_chromaticNumber_eq_zero into chromaticNumber_eq_zero_iff : G.chromaticNumber = 0 ↔ IsEmpty V and deprecate the → side
  • chromaticNumber_top_eq_enat_card: chromaticNumber ⊤ = ENat.card V
  • Tag chromaticNumber_top_eq_top_of_infinite/chromaticNumber_eq_zero_of_isEmpty as simp
  • Golf chromaticNumber_eq_one_iff

Estimated changes