Theorem SimpleGraph.Reachable.coe_dist_eq_edist

Modification history

2025-12-11 21:26
Mathlib/Combinatorics/SimpleGraph/Metric.lean
feat(Combinatorics/SimpleGraph/Acyclic): `IsAcyclic` -> `IsBipartite` (#32568) …
Added SimpleGraph.Reachable.coe_dist_eq_edistView on Github →