Commit 2025-12-07 18:24 c6741515

feat(Combinatorics/SimpleGraph): characterise containment of completeBipartiteGraph (#27602) Prove that a "left" subset of card α vertices and a "right" subset of card β vertices such that every vertex in the "left" subset is adjacent to every vertex in the "right" subset is equivalent to the containment of completeBipartiteGraph α β in G.