Chromatic Polynomial in Lean4

This is my first attempt at writing formal mathematics in Lean4. My goal is to define the chromatic polynomial of a simple graph, and then prove some elementary theorems about it.