Commit 2026-03-11 22:03 d8f22080

View on Github →

feat(Combinatorics/SimpleGraph/Hamiltonian): if mapping a Hamiltonian walk results in a path, the mapping function is injective (#36469)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean

added theorem SimpleGraph.Walk.IsHamiltonian.injective_of_isPath_map

modified theorem SimpleGraph.Walk.IsHamiltonian.map

modified theorem SimpleGraph.Walk.IsHamiltonian.mem_support

added theorem SimpleGraph.Walk.IsHamiltonian.setOf_support

deleted theorem SimpleGraph.Walk.IsHamiltonian.support_toFinset

added theorem SimpleGraph.Walk.IsHamiltonian.toFinset_support

modified theorem SimpleGraph.Walk.IsHamiltonianCycle.map

Modified Mathlib/Combinatorics/SimpleGraph/Paths.lean

added theorem SimpleGraph.Walk.IsPath.injOn_support_of_isPath_map