Commit 2026-10-13 09:24 d3313fc0

feat(SimpleGraph): hamiltonian cycle from cyclic permutation (#36376) This PR provides IsHamiltonian.of_perm: if σ is a cyclic permutation of a type with at least 3 elements, and each step v → σ v is an edge of G, then G is Hamiltonian. (Full support of σ is not assumed; it follows from G being loopless.) The proof goes through a more general statement, cycleGraph_isContained_of_isCycleOn: if σ is a cycle on a finset s and each v → σ v is an edge of G, then cycleGraph #s ⊑ G. The main theorem then follows from isHamiltonian_iff_cycleGraph_isContained. Also adds Equiv.Perm.IsCycleOn.injOn_pow_apply: the map n ↦ (f ^ n) a is injective on [0, #s).