Commit 2022-01-25 12:25 1b3da831

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.