Theorem SimpleGraph.IsCompleteMultipartite.completeBipartiteGraph

Modification history

2026-09-09 06:33
Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean
feat(Combinatorics/SimpleGraph): star graphs (and more) are bipartite (#43514) …
Added SimpleGraph.IsCompleteMultipartite.completeBipartiteGraphView on Github →