Commit 2026-09-09 06:33 763fa9e1

View on Github →

feat(Combinatorics/SimpleGraph): star graphs (and more) are bipartite (#43514) IsBipartite/IsBipartiteWith/IsCompleteBetween/IsCompleteMultipartite for completeBipartiteGraph/pathGraph/cycleGraph/⊥ (when applicable)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

added theorem SimpleGraph.IsCompleteBetween.completeBipartiteGraph

Modified Mathlib/Combinatorics/SimpleGraph/Bipartite.lean

added theorem SimpleGraph.IsBipartite.bot

added theorem SimpleGraph.IsBipartite.completeBipartiteGraph

Modified Mathlib/Combinatorics/SimpleGraph/Coloring/Constructions.lean

added theorem SimpleGraph.IsBipartite.cycleGraph_of_even

added theorem SimpleGraph.IsBipartite.pathGraph

Modified Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean

added theorem SimpleGraph.IsCompleteMultipartite.bot

added theorem SimpleGraph.IsCompleteMultipartite.completeBipartiteGraph

added theorem SimpleGraph.IsCompleteMultipartite.top

deleted theorem SimpleGraph.bot_isCompleteMultipartite

Modified Mathlib/Combinatorics/SimpleGraph/Star.lean

added def SimpleGraph.Coloring.starGraphBool

added theorem SimpleGraph.IsBipartite.starGraph

added theorem SimpleGraph.IsBipartiteWith.starGraph

added theorem SimpleGraph.IsCompleteBetween.starGraph

added theorem SimpleGraph.IsCompleteMultipartite.starGraph