Theorem SimpleGraph.Walk.IsTrail.nil_of_length_le_two

Modification history

2026-11-10 22:58
Mathlib/Combinatorics/SimpleGraph/Paths.lean
feat(Combinatorics/SimpleGraph/Paths): length of closed a walk/trail isn't `1`/`2` (#41633) …
Added SimpleGraph.Walk.IsTrail.nil_of_length_le_twoView on Github →