Theorem SimpleGraph.IsAcyclic.eq_snd_of_adj_start

Modification history

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.eq_snd_of_adj_startView on Github →