Commit 2026-01-02 14:40 e09bd04b

View on Github →

feat(Combinatorics/SimpleGraph/Acyclic): characterise maximal acyclic subgraphs (#32043) We characterise subgraphs H ≤ G which are maximal among acyclic subgraphs of G as those for which H.Reachable = G.Reachable. We also prove that if x and y are not reachable in G, then G ⊔ fromEdgeSet {s(x,y)} is acyclic iff G is.

Estimated changes