2026-08-16 09:33
Mathlib/Combinatorics/SimpleGraph/Paths.lean
feat(Combinatorics/SimpleGraph): add several lemmas about when `Walk.bypass` and `Walk.cycleBypass` do nothing (#37562)
Added SimpleGraph.Walk.IsTrail.length_cycleBypass_lt_iff_not_isCycle_and_not_nil