Commit 2026-10-17 12:17 bc0953a8

View on Github →

feat(SimpleGraph): reduce CycleGraph imports (#41306) Reduce the imports for CycleGraph.lean and re-prove and move a few lemmas around as a result.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean

added theorem SimpleGraph.Walk.reachable_of_mem_support

Modified Mathlib/Combinatorics/SimpleGraph/CycleGraph.lean

modified theorem SimpleGraph.connected_cycleGraph_add_one

added theorem SimpleGraph.cycleGraph.mem_support_cycle

added theorem SimpleGraph.cycleGraph_eq_top_iff

modified theorem SimpleGraph.cycleGraph_three_eq_top

modified theorem SimpleGraph.cycleGraph_two_eq_top

deleted theorem SimpleGraph.pathGraph_le_cycleGraph

modified theorem SimpleGraph.preconnected_cycleGraph

Modified Mathlib/Combinatorics/SimpleGraph/Hasse.lean

added theorem SimpleGraph.pathGraph_le_cycleGraph