Commit 2025-09-08 16:26 0ad288bf

View on Github →

chore(SimpleGraph/Walk): clean-up outlier variable block (#29394) This file uses u, v as the variable name for vertices almost everywhere. Get rid of this variable block and clean-up the few lemmas using it.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Walk.lean

modified theorem SimpleGraph.Walk.concat_dropLast

modified theorem SimpleGraph.Walk.cons_support_tail

modified theorem SimpleGraph.Walk.cons_tail_eq

modified theorem SimpleGraph.Walk.length_tail_add_one

modified theorem SimpleGraph.Walk.nil_copy

modified theorem SimpleGraph.Walk.support_tail