Theorem SimpleGraph.completeMultipartiteGraph.not_cliqueFree_of_le_enatCard

Modification history

2025-04-07 08:31
Mathlib/Combinatorics/SimpleGraph/Clique.lean
feat(Combinatorics/SimpleGraph): add facts about cliques and colorings of completeMultipartiteGraph (#21479) …
Added SimpleGraph.completeMultipartiteGraph.not_cliqueFree_of_le_enatCardView on Github →