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