Commit 2026-05-18 22:56 4438e0a0

View on Github →

feat(Combinatorics/SimpleGraph/Acyclic): endpoints of a path have at most one neighbor in the path (#37400)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

added theorem SimpleGraph.IsAcyclic.eq_penultimate_of_adj_end

added theorem SimpleGraph.IsAcyclic.eq_snd_of_adj_start

added theorem SimpleGraph.isAcyclic_iff_subsingleton_path