Rotate

📁 Source: Mathlib/Data/List/Rotate.lean

Statistics

Metric	Count
Definitions `IsRotated`, `setoid`, `cyclicPermutations`, `instDecidableR_mathlib`, `isRotatedDecidable`, `«term_~r_»`	6
Theorems `cons_append_singleton`, `cons_getLast_dropLast`, `cyclicPermutations`, `dropLast_tail`, `eqv`, `forall`, `map`, `mem_iff`, `nodup_iff`, `perm`, `refl`, `reverse`, `trans`, `cyclicPermutations`, `rotate_congr`, `rotate_congr_iff`, `rotate_eq_self_iff`, `cyclicPermutations_cons`, `cyclicPermutations_eq_nil_iff`, `cyclicPermutations_eq_singleton_iff`, `cyclicPermutations_inj`, `cyclicPermutations_injective`, `cyclicPermutations_ne_nil`, `cyclicPermutations_nil`, `cyclicPermutations_of_ne_nil`, `cyclicPermutations_rotate`, `getElem?_rotate`, `getElem_cyclicPermutations`, `getElem_eq_getElem_rotate`, `getElem_rotate`, `get_cyclicPermutations`, `get_eq_get_rotate`, `get_rotate`, `get_rotate_one`, `head?_cyclicPermutations`, `head?_rotate`, `head_cyclicPermutations`, `isRotated_append`, `isRotated_comm`, `isRotated_concat`, `isRotated_cyclicPermutations_iff`, `isRotated_iff_mem_map_range`, `isRotated_iff_mod`, `isRotated_nil_iff`, `isRotated_nil_iff'`, `isRotated_reverse_comm_iff`, `isRotated_reverse_iff`, `isRotated_singleton_iff`, `isRotated_singleton_iff'`, `length_cyclicPermutations_cons`, `length_cyclicPermutations_of_ne_nil`, `length_mem_cyclicPermutations`, `length_rotate`, `length_rotate'`, `map_rotate`, `mem_cyclicPermutations_iff`, `mem_cyclicPermutations_self`, `mem_rotate`, `nil_eq_rotate_iff`, `nodup_rotate`, `reverse_rotate`, `rotate'_cons_succ`, `rotate'_eq_drop_append_take`, `rotate'_length`, `rotate'_length_mul`, `rotate'_mod`, `rotate'_nil`, `rotate'_rotate'`, `rotate'_zero`, `rotate_append_length_eq`, `rotate_cons_succ`, `rotate_eq_drop_append_take`, `rotate_eq_drop_append_take_mod`, `rotate_eq_iff`, `rotate_eq_nil_iff`, `rotate_eq_rotate`, `rotate_eq_rotate'`, `rotate_eq_self_iff_eq_replicate`, `rotate_eq_singleton_iff`, `rotate_injective`, `rotate_length`, `rotate_length_mul`, `rotate_mod`, `rotate_nil`, `rotate_one_eq_self_iff_eq_replicate`, `rotate_perm`, `rotate_replicate`, `rotate_reverse`, `rotate_rotate`, `rotate_singleton`, `rotate_zero`, `singleton_eq_rotate_iff`, `zipWith_rotate_distrib`, `zipWith_rotate_one`	94
Total	100

List

Definitions

Name	Category	Theorems
`IsRotated` 📖	MathDef	27 math math: `isRotated_iff_mem_map_range`, `isRotated_comm`, `isRotated_append`, `isRotated_reverse_comm_iff`, `IsRotated.eqv`, `IsRotated.refl`, `SimpleGraph.Walk.rotate_edges`, `isRotated_concat`, `isRotated_nil_iff'`, `Cycle.coe_eq_coe`, `isRotated_iff_mod`, `Equiv.Perm.toList_formPerm_isRotated_self`, `isRotated_singleton_iff'`, `Equiv.Perm.SameCycle.toList_isRotated`, `isRotated_nil_iff`, `isRotated_singleton_iff`, `IsRotated.cons_append_singleton`, `IsRotated.cons_getLast_dropLast`, `SimpleGraph.Walk.support_rotate`, `isRotated_cyclicPermutations_iff`, `IsRotated.forall`, `mem_cyclicPermutations_iff`, `formPerm_eq_formPerm_iff`, `formPerm_ext_iff`, `isRotated_reverse_iff`, `IsRotated.dropLast_tail`, `SimpleGraph.Walk.rotate_darts`
`cyclicPermutations` 📖	CompOp	19 math math: `cyclicPermutations_eq_nil_iff`, `Nodup.cyclicPermutations`, `head_cyclicPermutations`, `cyclicPermutations_nil`, `get_cyclicPermutations`, `length_cyclicPermutations_of_ne_nil`, `length_cyclicPermutations_cons`, `head?_cyclicPermutations`, `cyclicPermutations_eq_singleton_iff`, `mem_cyclicPermutations_self`, `Cycle.lists_coe`, `IsRotated.cyclicPermutations`, `cyclicPermutations_cons`, `isRotated_cyclicPermutations_iff`, `cyclicPermutations_of_ne_nil`, `cyclicPermutations_injective`, `cyclicPermutations_rotate`, `mem_cyclicPermutations_iff`, `cyclicPermutations_inj`
`instDecidableR_mathlib` 📖	CompOp	—
`isRotatedDecidable` 📖	CompOp	—
`«term_~r_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cyclicPermutations_cons` 📖	mathematical	—	`cyclicPermutations`	—	—
`cyclicPermutations_eq_nil_iff` 📖	mathematical	—	`cyclicPermutations`	—	`cyclicPermutations_injective`
`cyclicPermutations_eq_singleton_iff` 📖	mathematical	—	`cyclicPermutations`	—	`cyclicPermutations_injective`
`cyclicPermutations_inj` 📖	mathematical	—	`cyclicPermutations`	—	`cyclicPermutations_injective`
`cyclicPermutations_injective` 📖	mathematical	—	`cyclicPermutations`	—	`head?_cyclicPermutations`
`cyclicPermutations_ne_nil` 📖	—	—	—	—	`length_cyclicPermutations_of_ne_nil`
`cyclicPermutations_nil` 📖	mathematical	—	`cyclicPermutations`	—	—
`cyclicPermutations_of_ne_nil` 📖	mathematical	—	`cyclicPermutations`	—	`cyclicPermutations_cons`
`cyclicPermutations_rotate` 📖	mathematical	—	`cyclicPermutations`	—	`rotate_nil` `rotate_singleton` `length_cyclicPermutations_of_ne_nil` `length_rotate` `get_rotate` `get_cyclicPermutations` `rotate_rotate` `rotate_mod` `getElem_cyclicPermutations`
`getElem?_rotate` 📖	—	—	—	—	`rotate_eq_drop_append_take_mod` `lt_or_ge` `LE.le.trans_lt` `LT.lt.le`
`getElem_cyclicPermutations` 📖	—	`cyclicPermutations`	—	—	`rotate_nil` `getElem_tails` `getElem_inits` `rotate_eq_drop_append_take` `length_cyclicPermutations_of_ne_nil` `LT.lt.le`
`getElem_eq_getElem_rotate` 📖	mathematical	—	`LT.lt.trans_eq` `LE.le.trans_lt` `Nat.instPreorder` `length_rotate`	—	`LT.lt.trans_eq` `LE.le.trans_lt` `length_rotate` `getElem_rotate` `LT.lt.le`
`getElem_rotate` 📖	mathematical	—	`LE.le.trans_lt` `Nat.instPreorder` `length_rotate`	—	`LE.le.trans_lt` `length_rotate` `getElem?_rotate` `LT.lt.trans_eq`
`get_cyclicPermutations` 📖	mathematical	—	`cyclicPermutations`	—	`getElem_cyclicPermutations`
`get_eq_get_rotate` 📖	mathematical	—	`LT.lt.trans_eq` `LE.le.trans_lt` `Nat.instPreorder` `length_rotate`	—	`LT.lt.trans_eq` `LE.le.trans_lt` `length_rotate` `getElem_eq_getElem_rotate`
`get_rotate` 📖	mathematical	—	`length_rotate`	—	`length_rotate` `LE.le.trans_lt` `getElem_rotate`
`get_rotate_one` 📖	mathematical	—	`length_rotate`	—	`get_rotate`
`head?_cyclicPermutations` 📖	mathematical	—	`cyclicPermutations`	—	`cyclicPermutations_ne_nil` `head_cyclicPermutations`
`head?_rotate` 📖	—	—	—	—	`getElem?_rotate` `LE.le.trans_lt`
`head_cyclicPermutations` 📖	mathematical	—	`cyclicPermutations` `cyclicPermutations_ne_nil`	—	`length_pos_of_ne_nil` `cyclicPermutations_ne_nil` `get_cyclicPermutations` `rotate_zero`
`isRotated_append` 📖	mathematical	—	`IsRotated`	—	`rotate_append_length_eq`
`isRotated_comm` 📖	mathematical	—	`IsRotated`	—	`IsRotated.symm`
`isRotated_concat` 📖	mathematical	—	`IsRotated`	—	`IsRotated.symm` `rotate_cons_succ` `rotate_zero`
`isRotated_cyclicPermutations_iff` 📖	mathematical	—	`IsRotated` `cyclicPermutations`	—	—
`isRotated_iff_mem_map_range` 📖	mathematical	—	`IsRotated`	—	—
`isRotated_iff_mod` 📖	mathematical	—	`IsRotated`	—	`rotate_nil` `LT.lt.le` `rotate_mod`
`isRotated_nil_iff` 📖	mathematical	—	`IsRotated`	—	`IsRotated.refl`
`isRotated_nil_iff'` 📖	mathematical	—	`IsRotated`	—	`isRotated_comm` `isRotated_nil_iff`
`isRotated_reverse_comm_iff` 📖	mathematical	—	`IsRotated`	—	`IsRotated.reverse`
`isRotated_reverse_iff` 📖	mathematical	—	`IsRotated`	—	—
`isRotated_singleton_iff` 📖	mathematical	—	`IsRotated`	—	`IsRotated.refl`
`isRotated_singleton_iff'` 📖	mathematical	—	`IsRotated`	—	`isRotated_comm` `isRotated_singleton_iff`
`length_cyclicPermutations_cons` 📖	mathematical	—	`cyclicPermutations`	—	`length_tails` `length_inits` `min_self`
`length_cyclicPermutations_of_ne_nil` 📖	mathematical	—	`cyclicPermutations`	—	`cyclicPermutations_of_ne_nil` `length_tails` `length_inits` `min_self`
`length_mem_cyclicPermutations` 📖	—	`cyclicPermutations`	—	—	`getElem_cyclicPermutations` `length_rotate`
`length_rotate` 📖	—	—	—	—	`rotate_eq_rotate'` `length_rotate'`
`length_rotate'` 📖	—	—	—	—	—
`map_rotate` 📖	—	—	—	—	`rotate_zero` `rotate_nil` `rotate_cons_succ`
`mem_cyclicPermutations_iff` 📖	mathematical	—	`cyclicPermutations` `IsRotated`	—	`get_cyclicPermutations` `IsRotated.forall` `cyclicPermutations_rotate` `mem_rotate` `mem_cyclicPermutations_self`
`mem_cyclicPermutations_self` 📖	mathematical	—	`cyclicPermutations`	—	`cyclicPermutations_ne_nil` `head_cyclicPermutations`
`mem_rotate` 📖	—	—	—	—	`rotate_nil` `rotate_zero` `rotate_cons_succ`
`nil_eq_rotate_iff` 📖	—	—	—	—	`rotate_eq_nil_iff`
`nodup_rotate` 📖	—	—	—	—	`rotate_perm`
`reverse_rotate` 📖	—	—	—	—	`rotate_eq_iff` `rotate_zero` `rotate_nil` `rotate_cons_succ` `rotate_rotate`
`rotate'_cons_succ` 📖	—	—	—	—	—
`rotate'_eq_drop_append_take` 📖	—	—	—	—	`rotate'_zero` `rotate'_cons_succ`
`rotate'_length` 📖	—	—	—	—	`rotate'_eq_drop_append_take` `le_rfl`
`rotate'_length_mul` 📖	—	—	—	—	`rotate'_zero` `length_rotate'` `rotate'_rotate'` `rotate'_length`
`rotate'_mod` 📖	—	—	—	—	`rotate'_length_mul` `rotate'_rotate'` `length_rotate'`
`rotate'_nil` 📖	—	—	—	—	—
`rotate'_rotate'` 📖	—	—	—	—	`rotate'_cons_succ`
`rotate'_zero` 📖	—	—	—	—	—
`rotate_append_length_eq` 📖	—	—	—	—	`rotate_eq_rotate'` `rotate'_zero`
`rotate_cons_succ` 📖	—	—	—	—	`rotate_eq_rotate'` `rotate'_cons_succ`
`rotate_eq_drop_append_take` 📖	—	—	—	—	`rotate_eq_rotate'` `rotate'_eq_drop_append_take`
`rotate_eq_drop_append_take_mod` 📖	—	—	—	—	`LE.le.eq_or_lt` `rotate_nil` `rotate_eq_drop_append_take` `LT.lt.le` `rotate_mod`
`rotate_eq_iff` 📖	—	—	—	—	`rotate_eq_rotate` `rotate_rotate` `rotate_mod` `LE.le.eq_or_lt` `rotate_nil` `rotate_zero` `LT.lt.le`
`rotate_eq_nil_iff` 📖	—	—	—	—	`rotate_zero` `rotate_nil` `rotate_cons_succ`
`rotate_eq_rotate` 📖	—	—	—	—	`rotate_injective`
`rotate_eq_rotate'` 📖	—	—	—	—	`rotate_nil` `rotate'_mod` `rotate'_eq_drop_append_take` `le_of_lt`
`rotate_eq_self_iff_eq_replicate` 📖	—	—	—	—	`rotate_nil` `head?_rotate` `rotate_replicate`
`rotate_eq_singleton_iff` 📖	—	—	—	—	`rotate_eq_iff` `rotate_singleton`
`rotate_injective` 📖	—	—	—	—	`length_rotate` `rotate_eq_drop_append_take_mod`
`rotate_length` 📖	—	—	—	—	`rotate_eq_rotate'` `rotate'_length`
`rotate_length_mul` 📖	—	—	—	—	`rotate_eq_rotate'` `rotate'_length_mul`
`rotate_mod` 📖	—	—	—	—	—
`rotate_nil` 📖	—	—	—	—	—
`rotate_one_eq_self_iff_eq_replicate` 📖	—	—	—	—	`rotate_eq_self_iff_eq_replicate` `rotate_zero` `rotate_rotate`
`rotate_perm` 📖	—	—	—	—	`rotate_eq_rotate'` `rotate'_zero` `rotate'_cons_succ`
`rotate_replicate` 📖	—	—	—	—	`length_rotate` `mem_rotate`
`rotate_reverse` 📖	—	—	—	—	`reverse_rotate` `rotate_rotate` `length_rotate` `rotate_zero` `rotate_length`
`rotate_rotate` 📖	—	—	—	—	`rotate_eq_rotate'` `rotate'_rotate'`
`rotate_singleton` 📖	—	—	—	—	`rotate_replicate`
`rotate_zero` 📖	—	—	—	—	—
`singleton_eq_rotate_iff` 📖	—	—	—	—	`rotate_eq_singleton_iff`
`zipWith_rotate_distrib` 📖	—	—	—	—	`rotate_eq_drop_append_take_mod` `min_self`
`zipWith_rotate_one` 📖	—	—	—	—	`rotate_cons_succ` `rotate_zero`

List.IsRotated

Definitions

Name	Category	Theorems
`setoid` 📖	CompOp	2 math math: `Cycle.mk_eq_coe`, `Cycle.mk''_eq_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cons_append_singleton` 📖	mathematical	—	`List.IsRotated`	—	`List.isRotated_append`
`cons_getLast_dropLast` 📖	mathematical	—	`List.IsRotated`	—	`symm` `List.isRotated_concat`
`cyclicPermutations` 📖	mathematical	`List.IsRotated`	`List.cyclicPermutations`	—	`List.cyclicPermutations_rotate`
`dropLast_tail` 📖	mathematical	—	`List.IsRotated`	—	—
`eqv` 📖	mathematical	—	`List.IsRotated`	—	`refl` `symm` `trans`
`forall` 📖	mathematical	—	`List.IsRotated`	—	`symm`
`map` 📖	—	`List.IsRotated`	—	—	`List.map_rotate`
`mem_iff` 📖	—	`List.IsRotated`	—	—	`perm`
`nodup_iff` 📖	—	`List.IsRotated`	—	—	`perm`
`perm` 📖	—	`List.IsRotated`	—	—	`List.rotate_perm`
`refl` 📖	mathematical	—	`List.IsRotated`	—	`List.rotate_zero`
`reverse` 📖	—	`List.IsRotated`	—	—	`List.reverse_rotate`
`trans` 📖	—	`List.IsRotated`	—	—	`List.rotate_rotate`

List.Nodup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cyclicPermutations` 📖	mathematical	—	`List.cyclicPermutations`	—	`eq_or_ne` `List.nodup_iff_injective_get` `List.getElem_cyclicPermutations` `rotate_congr_iff` `List.length_cyclicPermutations_of_ne_nil`
`rotate_congr` 📖	—	—	—	—	`List.length_pos_of_ne_nil` `List.head?_rotate` `getElem_inj_iff` `List.rotate_mod`
`rotate_congr_iff` 📖	—	—	—	—	`eq_or_ne` `List.rotate_nil` `rotate_congr` `List.rotate_mod`
`rotate_eq_self_iff` 📖	—	—	—	—	`rotate_congr_iff` `List.rotate_zero`

---

← Back to Index