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.isHamiltonian_iff_exists_adj_and_isHamiltonian