Theorem SimpleGraph.Walk.length_induce

Modification history

2026-11-10 14:10
Mathlib/Combinatorics/SimpleGraph/Walk/Maps.lean
feat(Combinatorics/SimpleGraph/Paths): some lemmas about inducing walks (#40967) …
Added SimpleGraph.Walk.length_induceView on Github →