Commit 2026-05-25 18:11 2a51a808

View on Github →

feat(Combinatorics/SimpleGraph/Walk/Paths): a trail which isn't a path has a cycle subwalk (#39061)

  • p.IsPath ↔ ∀ (v : V) (w : G.Walk v v), w.IsSubwalk p → w.Nil
  • p.IsTrail → (p.IsPath ↔ ∀ (v : V) (w : G.Walk v v), w.IsSubwalk p → ¬w.IsCycle)

Estimated changes