Commit 2026-11-10 14:10 dfab01f3

View on Github →

feat(Combinatorics/SimpleGraph/Paths): some lemmas about inducing walks (#40967) Could also be done via SimpleGraph.Walk.map_induce, but I thought that doing it directly is not much worse.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Paths.lean

added theorem SimpleGraph.Walk.isCircuit_induce

added theorem SimpleGraph.Walk.isCycle_induce

added theorem SimpleGraph.Walk.isPath_induce

added theorem SimpleGraph.Walk.isTrail_induce

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

added theorem SimpleGraph.Walk.darts_induce

added theorem SimpleGraph.Walk.edges_induce

added theorem SimpleGraph.Walk.length_induce

added theorem SimpleGraph.Walk.nil_induce

Modified Mathlib/Data/List/Nodup.lean

added theorem List.nodup_attachWith

Modified Mathlib/Data/Sym/Sym2.lean

added theorem Sym2.attachWith_inj

added theorem Sym2.attachWith_mk