Commit 2025-12-11 21:26 ad8efb3c

View on Github →

feat(Combinatorics/SimpleGraph/Acyclic): IsAcyclic -> IsBipartite (#32568) This generalizes the existing IsTree -> IsBipartite result.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

added theorem SimpleGraph.IsAcyclic.dist_eq_dist_add_one_of_adj_of_reachable

added theorem SimpleGraph.IsAcyclic.dist_ne_of_adj

added theorem SimpleGraph.IsAcyclic.isBipartite

deleted theorem SimpleGraph.IsTree.diff_dist_adj

added theorem SimpleGraph.IsTree.dist_eq_dist_add_one_of_adj

Modified Mathlib/Combinatorics/SimpleGraph/Metric.lean

added theorem SimpleGraph.Adj.diff_dist_adj

deleted theorem SimpleGraph.Connected.diff_dist_adj

added theorem SimpleGraph.Reachable.coe_dist_eq_edist

added theorem SimpleGraph.Reachable.dist_triangle_left

added theorem SimpleGraph.Reachable.dist_triangle_right