Commit 2026-09-30 15:24 bc9cca24

View on Github →

feat(Combinatorics/SimpleGraph/Hamiltonian): a graph with a Hamiltonian path is connected (#41435) and other small Hamiltonian lemmas.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean

modified theorem SimpleGraph.IsHamiltonian.connected

added theorem SimpleGraph.IsHamiltonian.nonempty

added theorem SimpleGraph.Walk.IsHamiltonian.connected

added theorem SimpleGraph.Walk.IsHamiltonian.copy

added theorem SimpleGraph.Walk.IsHamiltonian.isHamiltonian_of_nil

deleted theorem SimpleGraph.Walk.IsHamiltonian.map

added theorem SimpleGraph.Walk.IsHamiltonianCycle.connected

added theorem SimpleGraph.Walk.IsHamiltonianCycle.copy

added theorem SimpleGraph.Walk.IsHamiltonianCycle.isHamiltonian

added theorem SimpleGraph.Walk.IsHamiltonianCycle.isHamiltonian_dropLast

added theorem SimpleGraph.Walk.isHamiltonianCycle_copy

added theorem SimpleGraph.Walk.isHamiltonianCycle_iff_isCycle_and_forall_mem_support

added theorem SimpleGraph.Walk.isHamiltonianCycle_iff_isCycle_and_length_eq_natCard

added theorem SimpleGraph.Walk.isHamiltonianCycle_reverse

modified theorem SimpleGraph.Walk.isHamiltonianCycle_transfer

added theorem SimpleGraph.Walk.isHamiltonian_copy

added theorem SimpleGraph.Walk.isHamiltonian_dropLast_iff

added theorem SimpleGraph.Walk.isHamiltonian_iff_finite_and_isPath_and_length_eq

added theorem SimpleGraph.Walk.isHamiltonian_iff_isPath_and_forall_mem_support

added theorem SimpleGraph.Walk.isHamiltonian_map

added theorem SimpleGraph.Walk.isHamiltonian_mapLe

added theorem SimpleGraph.Walk.isHamiltonian_reverse

modified theorem SimpleGraph.Walk.isHamiltonian_transfer