mathlib3

4ce0899b - chore(combinatorics/simple_graph/coloring): remove extra asterisk (#10618)