Theorem SimpleGraph.Connected.diff_dist_adj

Modification history

2025-12-11 21:26

Mathlib/Combinatorics/SimpleGraph/Metric.lean

feat(Combinatorics/SimpleGraph/Acyclic): `IsAcyclic` -> `IsBipartite` (#32568) …

Deleted SimpleGraph.Connected.diff_dist_adj View on Github →

2025-09-28 13:29

Mathlib/Combinatorics/SimpleGraph/Metric.lean

feat(Combinatorics/SimpleGraph): add theorem `SimpleGraph.Connected.diff_dist_adj` (#27468) …

Added SimpleGraph.Connected.diff_dist_adj View on Github →