Theorem SimpleGraph.Walk.IsHamiltonian.isHamiltonian_of_adj

Modification history

2026-11-10 22:58
Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean
feat(SimpleGraph/Hamiltonian): a graph is Hamiltonian iff there's a Hamiltonian path with adjacent endpoints (#41393)
Added SimpleGraph.Walk.IsHamiltonian.isHamiltonian_of_adjView on Github →