Commit 2025-11-22 09:03 8a66b01b

feat(SimpleGraph): weaker condition for paths in acyclic graphs (#25814) IsAcyclic.isPath_iff_chain' defines a weaker condition for proving that a walk is a path, in particular it shows that rather than proving that all vertices in the support of a walk are distinct, one must only show that consecutive edges are distinct (e.g. every other vertex must be distinct.) This leads to a simple corollary that trails are also paths in acyclic graphs. I had a need for this when formalizing Cayley graphs, since this condition maps cleanly onto words in free groups being reduced.