Commit 2025-02-11 20:32 acfac8d1

View on Github →

feat(Combinatorics/SimpleGraph/Walk): add dropLast (#16382)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Walk.lean

added theorem SimpleGraph.Walk.concat_dropLast

added def SimpleGraph.Walk.dropLast

added theorem SimpleGraph.Walk.dropLast_concat

added theorem SimpleGraph.Walk.dropLast_cons_cons

added theorem SimpleGraph.Walk.dropLast_cons_nil

added theorem SimpleGraph.Walk.dropLast_cons_of_not_nil

added theorem SimpleGraph.Walk.dropLast_nil

added theorem SimpleGraph.Walk.getVert_mem_support

added theorem SimpleGraph.Walk.nil_reverse

added theorem SimpleGraph.Walk.penultimate_nil

added def SimpleGraph.Walk.take