2026-03-11 22:03
Mathlib/Combinatorics/SimpleGraph/Paths.lean
feat(Combinatorics/SimpleGraph/Hamiltonian): if mapping a Hamiltonian walk results in a path, the mapping function is injective (#36469)
Added SimpleGraph.Walk.IsPath.injOn_support_of_isPath_map