Commit 2026-04-28 16:44 44c34263

View on Github →

feat(SimpleGraph): cycleGraph.cycle is a cycle (#34797) (A follow-up PR will show that cycleGraph.cycle is also hamiltonian.)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Circulant.lean

added theorem SimpleGraph.cycleGraph.getVert_cycle

added theorem SimpleGraph.cycleGraph.isCycle_cycle

added theorem SimpleGraph.cycleGraph.isPath_tail_cycle

modified theorem SimpleGraph.cycleGraph.length_cycle