Def SimpleGraph.cycleGraph.cycle

Modification history

2026-06-30 21:02

Mathlib/Combinatorics/SimpleGraph/Circulant.lean

chore(SimpleGraph): move `cycleGraph` to its own file (#37930) …

Modified SimpleGraph.cycleGraph.cycle View on Github →

2026-03-19 16:26

Mathlib/Combinatorics/SimpleGraph/Circulant.lean

chore: rename `cycleGraph_EulerianCircuit` to `cycleGraph.cycle` (#35360) …

Added SimpleGraph.cycleGraph.cycle View on Github →