Cycle

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

Statistics

Metric	Count
Definitions `Cycle`, `decidableNontrivialCoe`, `fintypeNodupCycle`, `fintypeNodupNontrivialCycle`, `instCoeList`, `instDecidableEq`, `instDecidableMemOfDecidableEq`, `instDecidableNodup`, `instDecidableNontrivial`, `instEmptyCollection`, `instInhabited`, `instMembership`, `instRepr`, `length`, `lists`, `map`, `next`, `nil`, `ofList`, `prev`, `reverse`, `toFinset`, `toMultiset`, `next`, `nextOr`, `prev`	26
Theorems `eq_nil_of_irrefl`, `eq_nil_of_well_founded`, `imp`, `nil`, `nontrivial_iff`, `nodup`, `card_toMultiset`, `chain_coe_cons`, `chain_iff_pairwise`, `chain_map`, `chain_mono`, `chain_ne_nil`, `chain_of_pairwise`, `chain_range_succ`, `chain_singleton`, `coe_cons_eq_coe_append`, `coe_eq_coe`, `coe_eq_nil`, `coe_nil`, `coe_toFinset`, `coe_toMultiset`, `empty_eq`, `forall_eq_of_chain`, `induction_on`, `length_coe`, `length_nil`, `length_nontrivial`, `length_reverse`, `length_subsingleton_iff`, `lists_coe`, `lists_nil`, `map_coe`, `map_eq_nil`, `map_nil`, `mem_coe_iff`, `mem_lists_iff_coe_eq`, `mem_map`, `mem_reverse_iff`, `mk''_eq_coe`, `mk_eq_coe`, `next_mem`, `next_prev`, `next_reverse_eq_prev`, `next_reverse_eq_prev'`, `nil_toFinset`, `nil_toMultiset`, `nodup_coe_iff`, `nodup_nil`, `nodup_reverse_iff`, `nontrivial_coe_nodup_iff`, `nontrivial_reverse_iff`, `notMem_nil`, `prev_mem`, `prev_next`, `prev_reverse_eq_next`, `prev_reverse_eq_next'`, `reverse_coe`, `reverse_nil`, `reverse_reverse`, `subsingleton_nil`, `subsingleton_reverse_iff`, `toFinset_eq_nil`, `toFinset_toMultiset`, `toMultiset_eq_nil`, `isRotated_next_eq`, `isRotated_prev_eq`, `mem_of_nextOr_ne`, `nextOr_concat`, `nextOr_cons_of_ne`, `nextOr_eq_getElem?_idxOf_succ_of_mem_dropLast`, `nextOr_eq_getElem_idxOf_succ_of_mem_dropLast`, `nextOr_eq_nextOr_of_mem_dropLast`, `nextOr_eq_nextOr_of_mem_of_ne`, `nextOr_getLast_of_notMem_dropLast`, `nextOr_infix_of_mem_dropLast`, `nextOr_mem`, `nextOr_nil`, `nextOr_self_cons_cons`, `nextOr_singleton`, `next_cons_concat`, `next_cons_cons_eq`, `next_cons_cons_eq'`, `next_cons_eq_next_of_mem_dropLast`, `next_eq_getElem`, `next_getElem`, `next_getLast_cons`, `next_getLast_eq_head`, `next_getLast_eq_head_of_notMem_dropLast`, `next_mem`, `next_ne_head_ne_getLast`, `next_prev`, `next_reverse_eq_prev`, `next_singleton`, `pmap_next_eq_rotate_one`, `pmap_prev_eq_rotate_length_sub_one`, `prev_cons_cons_eq`, `prev_cons_cons_eq'`, `prev_cons_cons_of_ne`, `prev_cons_cons_of_ne'`, `prev_eq_getElem`, `prev_eq_getElem?_idxOf_pred_of_ne_head`, `prev_eq_getElem_idxOf_pred_of_ne_head`, `prev_getElem`, `prev_getLast_cons`, `prev_getLast_cons'`, `prev_head_eq_getLast`, `prev_infix_of_mem_tail`, `prev_mem`, `prev_ne_cons_cons`, `prev_next`, `prev_reverse_eq_next`, `prev_singleton`	112
Total	138

Cycle

Definitions

Name	Category	Theorems
`decidableNontrivialCoe` 📖	CompOp	—
`fintypeNodupCycle` 📖	CompOp	—
`fintypeNodupNontrivialCycle` 📖	CompOp	—
`instCoeList` 📖	CompOp	—
`instDecidableEq` 📖	CompOp	—
`instDecidableMemOfDecidableEq` 📖	CompOp	—
`instDecidableNodup` 📖	CompOp	—
`instDecidableNontrivial` 📖	CompOp	—
`instEmptyCollection` 📖	CompOp	1 math math: `empty_eq`
`instInhabited` 📖	CompOp	—
`instMembership` 📖	CompOp	8 math math: `mem_coe_iff`, `mem_reverse_iff`, `Equiv.Perm.mem_toCycle_iff_support`, `mem_map`, `Function.self_mem_periodicOrbit`, `notMem_nil`, `Function.iterate_mem_periodicOrbit`, `Function.mem_periodicOrbit_iff`
`instRepr` 📖	CompOp	—
`length` 📖	CompOp	7 math math: `length_nontrivial`, `Function.periodicOrbit_length`, `length_subsingleton_iff`, `length_coe`, `card_toMultiset`, `length_nil`, `length_reverse`
`lists` 📖	CompOp	3 math math: `mem_lists_iff_coe_eq`, `lists_coe`, `lists_nil`
`map` 📖	CompOp	6 math math: `map_nil`, `Function.periodicOrbit_eq_cycle_map`, `map_coe`, `mem_map`, `chain_map`, `map_eq_nil`
`next` 📖	CompOp	9 math math: `next_prev`, `next_reverse_eq_prev'`, `prev_reverse_eq_next'`, `next_mem`, `next_reverse_eq_prev`, `prev_next`, `formPerm_apply_mem_eq_next`, `Equiv.Perm.toCycle_next`, `prev_reverse_eq_next`
`nil` 📖	CompOp	20 math math: `toMultiset_eq_nil`, `Chain.nil`, `map_nil`, `nil_toFinset`, `nil_toMultiset`, `nodup_nil`, `toFinset_eq_nil`, `coe_eq_nil`, `Function.periodicOrbit_eq_nil_iff_not_periodic_pt`, `empty_eq`, `coe_nil`, `Chain.eq_nil_of_irrefl`, `Chain.eq_nil_of_well_founded`, `Function.periodicOrbit_eq_nil_of_not_periodic_pt`, `reverse_nil`, `subsingleton_nil`, `notMem_nil`, `lists_nil`, `length_nil`, `map_eq_nil`
`ofList` 📖	CompOp	26 math math: `mem_coe_iff`, `coe_toMultiset`, `Function.periodicOrbit_def`, `mem_lists_iff_coe_eq`, `coe_cons_eq_coe_append`, `Function.periodicOrbit_eq_cycle_map`, `mk_eq_coe`, `formPerm_coe`, `coe_eq_nil`, `chain_range_succ`, `coe_eq_coe`, `CartanMatrix.D_three'`, `map_coe`, `coe_toFinset`, `coe_nil`, `nodup_coe_iff`, `lists_coe`, `Equiv.Perm.toCycle_eq_toList`, `length_coe`, `mk''_eq_coe`, `chain_singleton`, `Equiv.Perm.exists_toCycle_toList`, `nontrivial_coe_nodup_iff`, `chain_coe_cons`, `chain_ne_nil`, `reverse_coe`
`prev` 📖	CompOp	7 math math: `next_prev`, `next_reverse_eq_prev'`, `prev_reverse_eq_next'`, `next_reverse_eq_prev`, `prev_next`, `prev_reverse_eq_next`, `prev_mem`
`reverse` 📖	CompOp	11 math math: `nodup_reverse_iff`, `mem_reverse_iff`, `nontrivial_reverse_iff`, `next_reverse_eq_prev`, `reverse_nil`, `subsingleton_reverse_iff`, `formPerm_reverse`, `prev_reverse_eq_next`, `reverse_reverse`, `reverse_coe`, `length_reverse`
`toFinset` 📖	CompOp	5 math math: `nil_toFinset`, `toFinset_eq_nil`, `support_formPerm`, `coe_toFinset`, `toFinset_toMultiset`
`toMultiset` 📖	CompOp	5 math math: `toMultiset_eq_nil`, `coe_toMultiset`, `nil_toMultiset`, `toFinset_toMultiset`, `card_toMultiset`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_toMultiset` 📖	mathematical	—	`Multiset.card` `toMultiset` `length`	—	`Quotient.inductionOn'`
`chain_coe_cons` 📖	mathematical	—	`Chain` `ofList`	—	—
`chain_iff_pairwise` 📖	mathematical	—	`Chain`	—	`induction_on` `notMem_nil` `instIsEmptyFalse` `chain_coe_cons` `trans` `chain_of_pairwise`
`chain_map` 📖	mathematical	—	`Chain` `map`	—	`List.isChain_cons_map`
`chain_mono` 📖	mathematical	—	`Monotone` `Pi.preorder` `PartialOrder.toPreorder` `Prop.partialOrder` `Cycle` `Chain`	—	`Chain.imp`
`chain_ne_nil` 📖	mathematical	—	`Chain` `ofList`	—	`coe_cons_eq_coe_append` `chain_coe_cons` `List.getLast_append_singleton`
`chain_of_pairwise` 📖	mathematical	—	`Chain`	—	`induction_on` `Chain.nil` `chain_coe_cons`
`chain_range_succ` 📖	mathematical	—	`Chain` `ofList`	—	`coe_cons_eq_coe_append` `chain_coe_cons` `List.isChain_cons_range_succ`
`chain_singleton` 📖	mathematical	—	`Chain` `ofList`	—	`chain_coe_cons` `List.isChain_pair`
`coe_cons_eq_coe_append` 📖	mathematical	—	`ofList`	—	`List.rotate_cons_succ` `List.rotate_zero`
`coe_eq_coe` 📖	mathematical	—	`ofList` `List.IsRotated`	—	`Quotient.eq`
`coe_eq_nil` 📖	mathematical	—	`ofList` `nil`	—	`coe_eq_coe` `List.isRotated_nil_iff`
`coe_nil` 📖	mathematical	—	`ofList` `nil`	—	—
`coe_toFinset` 📖	mathematical	—	`toFinset` `ofList` `List.toFinset`	—	—
`coe_toMultiset` 📖	mathematical	—	`toMultiset` `ofList` `Multiset.ofList`	—	—
`empty_eq` 📖	mathematical	—	`Cycle` `instEmptyCollection` `nil`	—	—
`forall_eq_of_chain` 📖	—	`Chain` `Cycle` `instMembership`	—	—	`antisymm` `chain_iff_pairwise`
`induction_on` 📖	—	`nil` `ofList`	—	—	`Quotient.inductionOn'`
`length_coe` 📖	mathematical	—	`length` `ofList`	—	—
`length_nil` 📖	mathematical	—	`length` `nil`	—	—
`length_nontrivial` 📖	mathematical	`Nontrivial`	`length`	—	—
`length_reverse` 📖	mathematical	—	`length` `reverse`	—	—
`length_subsingleton_iff` 📖	mathematical	—	`Subsingleton` `length`	—	—
`lists_coe` 📖	mathematical	—	`lists` `ofList` `Multiset.ofList` `List.cyclicPermutations`	—	—
`lists_nil` 📖	mathematical	—	`lists` `nil` `Multiset` `Multiset.instSingleton`	—	`nil.eq_1` `lists_coe` `List.cyclicPermutations_nil` `Multiset.coe_singleton`
`map_coe` 📖	mathematical	—	`map` `ofList`	—	—
`map_eq_nil` 📖	mathematical	—	`map` `nil`	—	`Quotient.inductionOn'`
`map_nil` 📖	mathematical	—	`map` `nil`	—	—
`mem_coe_iff` 📖	mathematical	—	`Cycle` `instMembership` `ofList`	—	—
`mem_lists_iff_coe_eq` 📖	mathematical	—	`Multiset` `Multiset.instMembership` `lists` `ofList`	—	`Quotient.inductionOn'` `lists.eq_1` `Quotient.liftOn'_mk''`
`mem_map` 📖	mathematical	—	`Cycle` `instMembership` `map`	—	`Quotient.inductionOn'`
`mem_reverse_iff` 📖	mathematical	—	`Cycle` `instMembership` `reverse`	—	—
`mk''_eq_coe` 📖	mathematical	—	`Quotient.mk''` `List.IsRotated.setoid` `ofList`	—	—
`mk_eq_coe` 📖	mathematical	—	`List.IsRotated.setoid` `ofList`	—	—
`next_mem` 📖	mathematical	`Nodup` `Cycle` `instMembership`	`next`	—	`List.next_mem`
`next_prev` 📖	mathematical	`Nodup` `Cycle` `instMembership`	`next` `prev` `prev_mem`	—	`Quotient.inductionOn'` `prev_mem` `List.next_prev`
`next_reverse_eq_prev` 📖	mathematical	`Nodup` `Cycle` `instMembership`	`next` `reverse` `nodup_reverse_iff` `mem_reverse_iff` `prev`	—	`nodup_reverse_iff` `mem_reverse_iff` `reverse_reverse` `prev.congr_simp`
`next_reverse_eq_prev'` 📖	mathematical	`Nodup` `reverse` `Cycle` `instMembership`	`next` `prev` `nodup_reverse_iff` `mem_reverse_iff`	—	`nodup_reverse_iff` `mem_reverse_iff` `reverse_reverse` `prev.congr_simp`
`nil_toFinset` 📖	mathematical	—	`toFinset` `nil` `Finset` `Finset.instEmptyCollection`	—	—
`nil_toMultiset` 📖	mathematical	—	`toMultiset` `nil` `Multiset` `Multiset.instZero`	—	—
`nodup_coe_iff` 📖	mathematical	—	`Nodup` `ofList`	—	—
`nodup_nil` 📖	mathematical	—	`Nodup` `nil`	—	—
`nodup_reverse_iff` 📖	mathematical	—	`Nodup` `reverse`	—	`List.nodup_reverse`
`nontrivial_coe_nodup_iff` 📖	mathematical	—	`Nontrivial` `ofList`	—	`Nontrivial.eq_1` `zero_add`
`nontrivial_reverse_iff` 📖	mathematical	—	`Nontrivial` `reverse`	—	—
`notMem_nil` 📖	mathematical	—	`Cycle` `instMembership` `nil`	—	—
`prev_mem` 📖	mathematical	`Nodup` `Cycle` `instMembership`	`prev`	—	`nodup_reverse_iff` `mem_reverse_iff` `next_reverse_eq_prev` `next_mem`
`prev_next` 📖	mathematical	`Nodup` `Cycle` `instMembership`	`prev` `next` `next_mem`	—	`Quotient.inductionOn'` `next_mem` `List.prev_next`
`prev_reverse_eq_next` 📖	mathematical	`Nodup` `Cycle` `instMembership`	`prev` `reverse` `nodup_reverse_iff` `mem_reverse_iff` `next`	—	`Quotient.inductionOn'` `nodup_reverse_iff` `mem_reverse_iff` `List.prev_reverse_eq_next`
`prev_reverse_eq_next'` 📖	mathematical	`Nodup` `reverse` `Cycle` `instMembership`	`prev` `next` `nodup_reverse_iff` `mem_reverse_iff`	—	`prev_reverse_eq_next` `nodup_reverse_iff` `mem_reverse_iff`
`reverse_coe` 📖	mathematical	—	`reverse` `ofList`	—	—
`reverse_nil` 📖	mathematical	—	`reverse` `nil`	—	—
`reverse_reverse` 📖	mathematical	—	`reverse`	—	—
`subsingleton_nil` 📖	mathematical	—	`Subsingleton` `nil`	—	—
`subsingleton_reverse_iff` 📖	mathematical	—	`Subsingleton` `reverse`	—	`length_reverse`
`toFinset_eq_nil` 📖	mathematical	—	`toFinset` `Finset` `Finset.instEmptyCollection` `nil`	—	`Quotient.inductionOn'`
`toFinset_toMultiset` 📖	mathematical	—	`Multiset.toFinset` `toMultiset` `toFinset`	—	—
`toMultiset_eq_nil` 📖	mathematical	—	`toMultiset` `Multiset` `Multiset.instZero` `nil`	—	`Quotient.inductionOn'`

Cycle.Chain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_nil_of_irrefl` 📖	mathematical	`Cycle.Chain`	`Cycle.nil`	—	`Cycle.induction_on` `irrefl_of` `Cycle.chain_iff_pairwise`
`eq_nil_of_well_founded` 📖	mathematical	`Cycle.Chain`	`Cycle.nil`	—	`eq_nil_of_irrefl` `Relation.instIsTransTransGen` `instAsymmOfIsWellFounded` `instIsWellFoundedTransGen` `imp`
`imp` 📖	—	`Cycle.Chain`	—	—	`Cycle.induction_on` `Cycle.chain_coe_cons`
`nil` 📖	mathematical	—	`Cycle.Chain` `Cycle.nil`	—	—

Cycle.Nodup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nontrivial_iff` 📖	mathematical	`Cycle.Nodup`	`Cycle.Nontrivial` `Cycle.Subsingleton`	—	`Cycle.length_subsingleton_iff` `Quotient.inductionOn'`

Cycle.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nodup` 📖	mathematical	`Cycle.Subsingleton`	`Cycle.Nodup`	—	—

List

Definitions

Name	Category	Theorems
`next` 📖	CompOp	20 math math: `next_eq_getElem`, `prev_next`, `next_getLast_eq_head`, `next_cons_cons_eq'`, `Equiv.Perm.next_toList_eq_apply`, `next_mem`, `isRotated_next_eq`, `next_reverse_eq_prev`, `next_prev`, `next_cons_eq_next_of_mem_dropLast`, `next_cons_concat`, `prev_reverse_eq_next`, `next_ne_head_ne_getLast`, `next_getElem`, `next_getLast_cons`, `next_getLast_eq_head_of_notMem_dropLast`, `next_singleton`, `formPerm_apply_mem_eq_next`, `next_cons_cons_eq`, `pmap_next_eq_rotate_one`
`nextOr` 📖	CompOp	12 math math: `nextOr_concat`, `nextOr_eq_nextOr_of_mem_dropLast`, `nextOr_infix_of_mem_dropLast`, `nextOr_mem`, `nextOr_nil`, `nextOr_cons_of_ne`, `nextOr_self_cons_cons`, `nextOr_singleton`, `nextOr_getLast_of_notMem_dropLast`, `nextOr_eq_getElem?_idxOf_succ_of_mem_dropLast`, `nextOr_eq_nextOr_of_mem_of_ne`, `nextOr_eq_getElem_idxOf_succ_of_mem_dropLast`
`prev` 📖	CompOp	21 math math: `prev_next`, `prev_ne_cons_cons`, `prev_mem`, `prev_eq_getElem?_idxOf_pred_of_ne_head`, `prev_infix_of_mem_tail`, `prev_cons_cons_eq'`, `prev_singleton`, `prev_getLast_cons'`, `next_reverse_eq_prev`, `prev_getLast_cons`, `next_prev`, `prev_cons_cons_eq`, `isRotated_prev_eq`, `prev_reverse_eq_next`, `prev_eq_getElem_idxOf_pred_of_ne_head`, `pmap_prev_eq_rotate_length_sub_one`, `prev_getElem`, `prev_eq_getElem`, `prev_head_eq_getLast`, `prev_cons_cons_of_ne'`, `prev_cons_cons_of_ne`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isRotated_next_eq` 📖	mathematical	`IsRotated`	`next` `IsRotated.mem_iff`	—	`IsRotated.mem_iff` `LE.le.trans_lt` `next_getElem` `LT.lt.trans_eq` `length_rotate` `getElem_eq_getElem_rotate` `next.congr_simp` `IsRotated.nodup_iff` `add_assoc`
`isRotated_prev_eq` 📖	mathematical	`IsRotated`	`prev` `IsRotated.mem_iff`	—	`IsRotated.mem_iff` `next_reverse_eq_prev` `IsRotated.nodup_iff` `isRotated_next_eq` `IsRotated.reverse` `nodup_reverse`
`mem_of_nextOr_ne` 📖	—	—	—	—	`nextOr_cons_of_ne`
`nextOr_concat` 📖	mathematical	—	`nextOr`	—	`nextOr_cons_of_ne`
`nextOr_cons_of_ne` 📖	mathematical	—	`nextOr`	—	—
`nextOr_eq_getElem?_idxOf_succ_of_mem_dropLast` 📖	mathematical	—	`nextOr`	—	`nextOr.eq_3` `idxOf_cons_ne`
`nextOr_eq_getElem_idxOf_succ_of_mem_dropLast` 📖	mathematical	—	`nextOr` `succ_idxOf_lt_length_of_mem_dropLast`	—	`Option.some_injective` `succ_idxOf_lt_length_of_mem_dropLast` `nextOr_eq_getElem?_idxOf_succ_of_mem_dropLast`
`nextOr_eq_nextOr_of_mem_dropLast` 📖	mathematical	—	`nextOr`	—	`nextOr_self_cons_cons` `nextOr.eq_3`
`nextOr_eq_nextOr_of_mem_of_ne` 📖	mathematical	—	`nextOr`	—	`nextOr_eq_nextOr_of_mem_dropLast`
`nextOr_getLast_of_notMem_dropLast` 📖	mathematical	—	`nextOr`	—	`nextOr.eq_def`
`nextOr_infix_of_mem_dropLast` 📖	mathematical	—	`nextOr`	—	—
`nextOr_mem` 📖	mathematical	—	`nextOr`	—	`nextOr.eq_3`
`nextOr_nil` 📖	mathematical	—	`nextOr`	—	—
`nextOr_self_cons_cons` 📖	mathematical	—	`nextOr`	—	—
`nextOr_singleton` 📖	mathematical	—	`nextOr`	—	—
`next_cons_concat` 📖	mathematical	—	`next`	—	`next.eq_1` `nextOr_concat` `zero_add`
`next_cons_cons_eq` 📖	mathematical	—	`next`	—	`next_cons_cons_eq'`
`next_cons_cons_eq'` 📖	mathematical	—	`next`	—	`next.eq_1` `nextOr.eq_3`
`next_cons_eq_next_of_mem_dropLast` 📖	mathematical	—	`next` `mem_of_mem_dropLast`	—	`mem_of_mem_dropLast` `next.eq_1` `nextOr_cons_of_ne` `nextOr_eq_nextOr_of_mem_dropLast`
`next_eq_getElem` 📖	mathematical	—	`next`	—	`succ_idxOf_lt_length_of_mem_dropLast` `nextOr_eq_getElem_idxOf_succ_of_mem_dropLast`
`next_getElem` 📖	mathematical	—	`next` `LE.le.trans_lt` `Nat.instPreorder`	—	—
`next_getLast_cons` 📖	mathematical	—	`next`	—	`next.eq_1` `dropLast_append_getLast` `nextOr_concat` `nodup_iff_injective_get`
`next_getLast_eq_head` 📖	mathematical	—	`next`	—	`LE.le.trans_lt` `next.congr_simp` `next_getElem`
`next_getLast_eq_head_of_notMem_dropLast` 📖	mathematical	—	`next`	—	`nextOr_getLast_of_notMem_dropLast`
`next_mem` 📖	mathematical	—	`next`	—	`nextOr_mem`
`next_ne_head_ne_getLast` 📖	mathematical	—	`next` `mem_of_mem_dropLast`	—	`next_cons_eq_next_of_mem_dropLast`
`next_prev` 📖	mathematical	—	`next` `prev` `prev_mem`	—	`prev_mem` `LE.le.trans_lt` `prev_getElem` `next.congr_simp` `next_getElem` `add_assoc`
`next_reverse_eq_prev` 📖	mathematical	—	`next` `prev`	—	`prev_reverse_eq_next` `nodup_reverse`
`next_singleton` 📖	mathematical	—	`next`	—	—
`pmap_next_eq_rotate_one` 📖	mathematical	—	`next`	—	`length_rotate` `LE.le.trans_lt` `getElem_rotate` `next_getElem`
`pmap_prev_eq_rotate_length_sub_one` 📖	mathematical	—	`prev`	—	`length_rotate` `LE.le.trans_lt` `getElem_rotate` `prev_getElem`
`prev_cons_cons_eq` 📖	mathematical	—	`prev`	—	`prev_cons_cons_eq'`
`prev_cons_cons_eq'` 📖	mathematical	—	`prev`	—	`prev.eq_3`
`prev_cons_cons_of_ne` 📖	mathematical	—	`prev`	—	`prev_cons_cons_of_ne'`
`prev_cons_cons_of_ne'` 📖	mathematical	—	`prev`	—	`prev.eq_3`
`prev_eq_getElem` 📖	mathematical	—	`prev`	—	`zero_add` `prev_getLast_cons` `prev_eq_getElem_idxOf_pred_of_ne_head`
`prev_eq_getElem?_idxOf_pred_of_ne_head` 📖	mathematical	—	`prev`	—	—
`prev_eq_getElem_idxOf_pred_of_ne_head` 📖	mathematical	—	`prev`	—	`Option.some_injective` `prev_eq_getElem?_idxOf_pred_of_ne_head`
`prev_getElem` 📖	mathematical	—	`prev`	—	—
`prev_getLast_cons` 📖	mathematical	—	`prev`	—	`prev_getLast_cons'`
`prev_getLast_cons'` 📖	mathematical	—	`prev`	—	—
`prev_head_eq_getLast` 📖	mathematical	—	`prev`	—	`prev_getLast_cons`
`prev_infix_of_mem_tail` 📖	mathematical	—	`prev`	—	`idxOf_cons_ne`
`prev_mem` 📖	mathematical	—	`prev`	—	`prev.congr_simp` `prev_cons_cons_eq` `prev.eq_3`
`prev_ne_cons_cons` 📖	mathematical	—	`prev`	—	`prev.eq_3`
`prev_next` 📖	mathematical	—	`prev` `next` `next_mem`	—	`next_mem` `LE.le.trans_lt` `next_getElem` `prev.congr_simp` `prev_getElem` `add_assoc` `add_comm`
`prev_reverse_eq_next` 📖	mathematical	—	`prev` `next`	—	`LE.le.trans_lt` `prev.congr_simp` `pmap_next_eq_rotate_one` `pmap_prev_eq_rotate_length_sub_one` `nodup_reverse` `rotate_reverse` `Nat.succ_pos'` `zero_add` `length_rotate`
`prev_singleton` 📖	mathematical	—	`prev`	—	—

(root)

Definitions

Name	Category	Theorems
`Cycle` 📖	CompOp	13 math math: `Cycle.mem_coe_iff`, `Cycle.mem_reverse_iff`, `Equiv.Perm.IsCycle.existsUnique_cycle_nontrivial_subtype`, `Equiv.Perm.mem_toCycle_iff_support`, `Cycle.empty_eq`, `Equiv.Perm.IsCycle.existsUnique_cycle_subtype`, `Cycle.mem_map`, `Function.self_mem_periodicOrbit`, `Cycle.chain_mono`, `Equiv.Perm.IsCycle.existsUnique_cycle`, `Cycle.notMem_nil`, `Function.iterate_mem_periodicOrbit`, `Function.mem_periodicOrbit_iff`

---

← Back to Index