Theorem SimpleGraph.IsAcyclic.eq_penultimate_of_adj_end

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_penultimate_of_adj_endView on Github →