Theorem SimpleGraph.isAcyclic_add_edge_iff_of_not_reachable

Modification history

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