Theorem SimpleGraph.maximal_isAcyclic_iff_reachable_eq

Modification history

2026-03-01 13:37

Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

feat(Combinatorics/SimpleGraph/Acyclic): acyclic and bridge theorems + golfing (#30640)

Modified SimpleGraph.maximal_isAcyclic_iff_reachable_eq View on Github →

2026-01-02 14:40

Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

feat(Combinatorics/SimpleGraph/Acyclic): characterise maximal acyclic subgraphs (#32043) …

Added SimpleGraph.maximal_isAcyclic_iff_reachable_eq View on Github →