Theorem SimpleGraph.reachable_eq_of_maximal_isAcyclic

Modification history

2026-01-02 14:40
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
feat(Combinatorics/SimpleGraph/Acyclic): characterise maximal acyclic subgraphs (#32043) …
Added SimpleGraph.reachable_eq_of_maximal_isAcyclicView on Github →