Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-16 15:31 a564bf1e

View on Github →

feat(data/list/cycle): cycles as quotients of lists (#7504) Cycles are common structures, and we define them as a quotient of lists. This is on the route to defining concrete cyclic permutations, and could also be used for encoding properties of cycles in graphs.

Estimated changes

added theorem cycle.coe_eq_coe
added def cycle.length
added theorem cycle.length_coe
added theorem cycle.length_reverse
added def cycle.mem
added theorem cycle.mem_coe_iff
added theorem cycle.mem_reverse_iff
added theorem cycle.mk'_eq_coe
added theorem cycle.mk_eq_coe
added def cycle.next
added theorem cycle.next_mem
added def cycle.nodup
added theorem cycle.nodup_coe_iff
added def cycle.nontrivial
added def cycle.prev
added theorem cycle.prev_mem
added def cycle.reverse
added theorem cycle.reverse_coe
added theorem cycle.reverse_reverse
added def cycle.to_finset
added def cycle
added theorem list.mem_of_next_or_ne
added def list.next
added theorem list.next_cons_concat
added theorem list.next_cons_cons_eq
added theorem list.next_last_cons
added theorem list.next_mem
added theorem list.next_nth_le
added def list.next_or
added theorem list.next_or_concat
added theorem list.next_or_mem
added theorem list.next_or_nil
added theorem list.next_or_singleton
added theorem list.next_prev
added theorem list.next_singleton
added def list.prev
added theorem list.prev_cons_cons_eq
added theorem list.prev_last_cons'
added theorem list.prev_last_cons
added theorem list.prev_mem
added theorem list.prev_ne_cons_cons
added theorem list.prev_next
added theorem list.prev_nth_le
added theorem list.prev_singleton
added theorem list.nth_le_rotate'
added theorem list.rotate_reverse