Theorem SimpleGraph.IsAcyclic.dist_ne_of_adj

Modification history

2025-12-11 21:26

Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

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

Added SimpleGraph.IsAcyclic.dist_ne_of_adj View on Github →