Commit 2025-07-02 23:52 2eda5e74

View on Github →

feat(SimpleGraph): Helper lemmas for Walk.take/drop (#25650) Contributing helper lemmas I needed when formalizing Cayley graphs.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Walk.lean

added theorem SimpleGraph.Walk.drop_getVert

added theorem SimpleGraph.Walk.drop_length

added theorem SimpleGraph.Walk.take_getVert

added theorem SimpleGraph.Walk.take_length