Commit 2026-03-19 16:26 eccb236b

View on Github →

chore: rename cycleGraph_EulerianCircuit to cycleGraph.cycle (#35360) Per this review feedback, this definition is inappropriately named with an underscore and should be renamed.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Circulant.lean

added def SimpleGraph.cycleGraph.cycle

added theorem SimpleGraph.cycleGraph.length_cycle

deleted def SimpleGraph.cycleGraph_EulerianCircuit

deleted theorem SimpleGraph.cycleGraph_EulerianCircuit_length

Modified Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean