Theorem SimpleGraph.completeMultipartiteGraph.not_cliqueFree_of_le_card

Modification history

2026-01-30 13:30

Mathlib/Combinatorics/SimpleGraph/Clique.lean

feat(Combinatorics/SimpleGraph/Clique): avoid `Fintype`/`Finite` assumptions where possible (#33253) …

Modified SimpleGraph.completeMultipartiteGraph.not_cliqueFree_of_le_card View on Github →

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_card View on Github →