From 90f348ac1e77c9e655f5f3ba519bd3c210dc5653 Mon Sep 17 00:00:00 2001
From: jt496 <john.talbot@gmail.com>
Date: Tue, 28 Jan 2025 16:37:30 +0000
Subject: [PATCH] colorable_zero_iff

---
 Mathlib/Combinatorics/SimpleGraph/Coloring.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Coloring.lean b/Mathlib/Combinatorics/SimpleGraph/Coloring.lean
index 54483becc0906..3a7e6f287d154 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Coloring.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Coloring.lean
@@ -137,6 +137,10 @@ theorem isEmpty_of_colorable_zero (h : G.Colorable 0) : IsEmpty V := by
   obtain ⟨i, hi⟩ := h.some v
   exact Nat.not_lt_zero _ hi
 
+@[simp]
+lemma colorable_zero_iff : G.Colorable 0 ↔ IsEmpty V :=
+   ⟨fun h => G.isEmpty_of_colorable_zero h, fun _ => G.colorable_of_isEmpty 0⟩
+
 /-- The "tautological" coloring of a graph, using the vertices of the graph as colors. -/
 def selfColoring : G.Coloring V := Coloring.mk id fun {_ _} => G.ne_of_adj