Theorem SimpleGraph.Walk.IsHamiltonian.length_add_one_eq

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.length_add_one_eqView on Github →