Commit 2026-06-30 21:02 d6e37a2f

View on Github →

chore(SimpleGraph): move cycleGraph to its own file (#37930) PR #34797 re-defined cycleGraph independent of circulantGraph. Now move the definition of cycleGraph to its own file so that the definition can be used without importing the algebra hierarchy.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Combinatorics/SimpleGraph/Circulant.lean

deleted def SimpleGraph.cycleGraph.cycle

deleted theorem SimpleGraph.cycleGraph.getVert_cycle

deleted theorem SimpleGraph.cycleGraph.isCycle_cycle

deleted theorem SimpleGraph.cycleGraph.isPath_tail_cycle

deleted theorem SimpleGraph.cycleGraph.length_cycle

deleted def SimpleGraph.cycleGraph

deleted theorem SimpleGraph.cycleGraph_adj'

deleted theorem SimpleGraph.cycleGraph_adj

deleted theorem SimpleGraph.cycleGraph_connected

deleted theorem SimpleGraph.cycleGraph_degree_three_le

deleted theorem SimpleGraph.cycleGraph_degree_two_le

deleted theorem SimpleGraph.cycleGraph_neighborFinset

deleted theorem SimpleGraph.cycleGraph_neighborSet

deleted theorem SimpleGraph.cycleGraph_one_adj

deleted theorem SimpleGraph.cycleGraph_one_eq_bot

deleted theorem SimpleGraph.cycleGraph_one_eq_top

deleted theorem SimpleGraph.cycleGraph_preconnected

deleted theorem SimpleGraph.cycleGraph_three_eq_top

deleted theorem SimpleGraph.cycleGraph_two_eq_top

deleted theorem SimpleGraph.cycleGraph_zero_adj

deleted theorem SimpleGraph.cycleGraph_zero_eq_bot

deleted theorem SimpleGraph.cycleGraph_zero_eq_top

deleted theorem SimpleGraph.pathGraph_le_cycleGraph

Created Mathlib/Combinatorics/SimpleGraph/CycleGraph.lean

added def SimpleGraph.cycleGraph.cycle

added theorem SimpleGraph.cycleGraph.getVert_cycle

added theorem SimpleGraph.cycleGraph.isCycle_cycle

added theorem SimpleGraph.cycleGraph.isPath_tail_cycle

added theorem SimpleGraph.cycleGraph.length_cycle

added def SimpleGraph.cycleGraph

added theorem SimpleGraph.cycleGraph_adj'

added theorem SimpleGraph.cycleGraph_adj

added theorem SimpleGraph.cycleGraph_connected

added theorem SimpleGraph.cycleGraph_degree_three_le

added theorem SimpleGraph.cycleGraph_degree_two_le

added theorem SimpleGraph.cycleGraph_neighborFinset

added theorem SimpleGraph.cycleGraph_neighborSet

added theorem SimpleGraph.cycleGraph_one_adj

added theorem SimpleGraph.cycleGraph_one_eq_bot

added theorem SimpleGraph.cycleGraph_one_eq_top

added theorem SimpleGraph.cycleGraph_preconnected

added theorem SimpleGraph.cycleGraph_three_eq_top

added theorem SimpleGraph.cycleGraph_two_eq_top

added theorem SimpleGraph.cycleGraph_zero_adj

added theorem SimpleGraph.cycleGraph_zero_eq_bot

added theorem SimpleGraph.cycleGraph_zero_eq_top

added theorem SimpleGraph.pathGraph_le_cycleGraph