Commit 2026-11-10 22:58 f592d119

View on Github →

feat(SimpleGraph/Hamiltonian): a graph is Hamiltonian iff there's a Hamiltonian path with adjacent endpoints (#41393)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean

added theorem SimpleGraph.Walk.IsHamiltonian.isHamiltonian_of_adj

added theorem SimpleGraph.Walk.IsHamiltonian.length_add_one_eq

added theorem SimpleGraph.Walk.isHamiltonianCycle_iff_isHamiltonian_tail_and_le_card

added theorem SimpleGraph.isHamiltonian_iff_exists_adj_and_isHamiltonian