Theorems · Definition · combinatorics
SimpleGraph.Walk.rotate
{V : Type u} → {G : SimpleGraph V} → {v : V} → [DecidableEq V] → (c : G.Walk v v) → (u : V) → u ∈ c.support → G.Walk u uRotate a loop walk such that it is centered at the given vertex.
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext
- Assumes
- DecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SimpleGraphstatement and proof · cited by 3,072
- SimpleGraph.Walkstatement and proof · cited by 915
- SimpleGraph.Walk.supportstatement and proof · cited by 307
- SimpleGraph.Walk.appendproof · cited by 95
- SimpleGraph.Walk.takeUntilproof · cited by 58
- SimpleGraph.Walk.dropUntilproof · cited by 38
Cited by25
Results whose statement or proof uses this declaration.
- SimpleGraph.Walk.rotate_edgesstatement · cited by 3
- SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycleproof · cited by 3
- SimpleGraph.Walk.isTrail_rotatestatement and proof · cited by 2
- SimpleGraph.Walk.isCircuit_rotatestatement and proof · cited by 2
- SimpleGraph.Walk.isCycle_rotatestatement and proof · cited by 2
- SimpleGraph.Walk.isHamiltonianCycle_rotatestatement · cited by 2
- SimpleGraph.Walk.length_rotatestatement and proof · cited by 2
- SimpleGraph.Walk.IsCycle.rotatestatement · cited by 2
- SimpleGraph.Walk.rotate_dartsstatement · cited by 1
- SimpleGraph.IsHamiltonian.exists_isHamiltonianCycleproof · cited by 1
- SimpleGraph.Walk.IsTrail.rotatestatement · cited by 1
- SimpleGraph.exists_isCycle_of_two_le_isEdgeReachableproof · cited by 1