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