Theorem SimpleGraph.Walk.isHamiltonian_iff_support_get_bijective

Modification history

2025-11-04 06:22
Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean
feat(Combinatorics/SimpleGraph/Hamiltonian): `p.support.get` is bijective (#30224)
Added SimpleGraph.Walk.isHamiltonian_iff_support_get_bijectiveView on Github →