Commit 2026-09-14 23:00 2a92623d

View on Github →

feat(Combinatorics/SimpleGraph/Walk): more transfer API (#41717)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean

added theorem SimpleGraph.Walk.isHamiltonianCycle_transfer

added theorem SimpleGraph.Walk.isHamiltonian_transfer

Modified Mathlib/Combinatorics/SimpleGraph/Paths.lean

added theorem SimpleGraph.Walk.isCircuit_transfer

added theorem SimpleGraph.Walk.isCycle_transfer

added theorem SimpleGraph.Walk.isPath_transfer

added theorem SimpleGraph.Walk.isTrail_transfer

Modified Mathlib/Combinatorics/SimpleGraph/Walk/Maps.lean

added theorem SimpleGraph.Walk.mapLe_toDeleteEdges_eq

deleted theorem SimpleGraph.Walk.map_toDeleteEdges_eq

added theorem SimpleGraph.Walk.nil_transfer

added theorem SimpleGraph.Walk.transfer_eq_mapLe

deleted theorem SimpleGraph.Walk.transfer_eq_map_ofLE