Commit 2026-04-01 13:58 fefd1c26

View on Github →

feat(Combinatorics/SimpleGraph/Walk/Operations): clean up append/concat (#36705) _ ++ [_] is the simpNF of List.concat _ _.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean

Modified Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean

Modified Mathlib/Combinatorics/SimpleGraph/Paths.lean

Modified Mathlib/Combinatorics/SimpleGraph/Walk/Basic.lean

added theorem SimpleGraph.Walk.cons_tail_support

Modified Mathlib/Combinatorics/SimpleGraph/Walk/Decomp.lean

Modified Mathlib/Combinatorics/SimpleGraph/Walk/Operations.lean

modified theorem SimpleGraph.Walk.concat_dropLast

modified theorem SimpleGraph.Walk.cons_support_tail

added theorem SimpleGraph.Walk.dropLast_support_concat

modified theorem SimpleGraph.Walk.support_concat

modified theorem SimpleGraph.Walk.support_eq_concat

Modified Mathlib/Combinatorics/SimpleGraph/Walk/Subwalks.lean