Theorem SimpleGraph.Walk.IsHamiltonian.map

Modification history

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)

Modified SimpleGraph.Walk.IsHamiltonian.map View on Github →

2024-06-07 11:39

Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean

feat: Define Hamiltonian paths and cycles (#7102)

Added SimpleGraph.Walk.IsHamiltonian.map View on Github →