Theorem SimpleGraph.bot_isCompleteMultipartite

Modification history

2026-09-09 06:33
Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean
feat(Combinatorics/SimpleGraph): star graphs (and more) are bipartite (#43514) …
Deleted SimpleGraph.bot_isCompleteMultipartiteView on Github →
2026-03-26 23:51
Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean
chore(Order/Defs/Unbundled): deprecate `def Transitive` in favor of `class IsTrans` (#35592)
Modified SimpleGraph.bot_isCompleteMultipartiteView on Github →
2025-08-20 10:00
Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean
feat(Combinatorics/SimpleGraph): define `completeEquipartiteGraph` (#27597) …
Added SimpleGraph.bot_isCompleteMultipartiteView on Github →