mathlib

1b3da831 - feat(combinatorics/simple_graph/coloring): add inequalities from embeddings (#11548)

feat(combinatorics/simple_graph/coloring): add inequalities from embeddings (#11548) Also add a lemma that the chromatic number of an infinite complete graph is zero (i.e., it needs infinitely many colors), as suggested by @arthurpaulino.