Theorems · Definition · combinatorics
List.IsRotated.setoid
(α : Type u_1) → Setoid (List α)
The relation List.IsRotated l l' forms a Setoid of cycles.
- Defined in
- Mathlib.Data.List.Rotate
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 59 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- List.IsRotatedproof · cited by 39
- List.IsRotated.eqvproof · cited by 0
Cited by4
Results whose statement or proof uses this declaration.
- Cycleproof · cited by 79
- Cycle.formPermproof · cited by 13
- Cycle.mk''_eq_coestatement · cited by 0
- Cycle.mk_eq_coestatement · cited by 0