Theorem SimpleGraph.isAcyclic_iff_subsingleton_path

Modification history

2026-07-14 11:01
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
chore(SimpleGraph/Acyclic): clean up "acyclic iff at most one path" API (#41219) …
Modified SimpleGraph.isAcyclic_iff_subsingleton_pathView on Github →
2026-05-18 22:56
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
feat(Combinatorics/SimpleGraph/Acyclic): endpoints of a path have at most one neighbor in the path (#37400)
Added SimpleGraph.isAcyclic_iff_subsingleton_pathView on Github →