Commit 2024-06-07 11:39 b4911b22

View on Github →

feat: Define Hamiltonian paths and cycles (#7102)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/BigOperators/Group/Finset.lean

added theorem List.sum_toFinset_count_eq_length

modified theorem Multiset.toFinset_sum_count_eq

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity.lean

added theorem SimpleGraph.Walk.IsCircuit.not_nil

added theorem SimpleGraph.Walk.IsCycle.not_nil

modified theorem SimpleGraph.Walk.cons_support_tail

added theorem SimpleGraph.Walk.nil_iff_eq_nil

added theorem SimpleGraph.Walk.support_tail

Created Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean

added theorem SimpleGraph.IsHamiltonian.connected

added theorem SimpleGraph.IsHamiltonian.mono

added def SimpleGraph.IsHamiltonian

added theorem SimpleGraph.Walk.IsHamiltonian.isPath

added theorem SimpleGraph.Walk.IsHamiltonian.length_eq

added theorem SimpleGraph.Walk.IsHamiltonian.map

added theorem SimpleGraph.Walk.IsHamiltonian.mem_support

added theorem SimpleGraph.Walk.IsHamiltonian.support_toFinset

added def SimpleGraph.Walk.IsHamiltonian

added theorem SimpleGraph.Walk.IsHamiltonianCycle.count_support_self

added theorem SimpleGraph.Walk.IsHamiltonianCycle.isCycle

added theorem SimpleGraph.Walk.IsHamiltonianCycle.length_eq

added theorem SimpleGraph.Walk.IsHamiltonianCycle.map

added theorem SimpleGraph.Walk.IsHamiltonianCycle.mem_support

added theorem SimpleGraph.Walk.IsHamiltonianCycle.support_count_of_ne

added structure SimpleGraph.Walk.IsHamiltonianCycle

added theorem SimpleGraph.Walk.IsPath.isHamiltonian_iff

added theorem SimpleGraph.Walk.IsPath.isHamiltonian_of_mem

added theorem SimpleGraph.Walk.isHamiltonianCycle_iff_isCycle_and_support_count_tail_eq_one

added theorem SimpleGraph.Walk.isHamiltonianCycle_isCycle_and_isHamiltonian_tail