Commit 2023-01-27 13:40 31dd00ce

View on Github →

feat: port Data.List.Cycle (#1642)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/List/Cycle.lean

added theorem Cycle.Chain.nil

added def Cycle.Mem

added theorem Cycle.Nodup.nontrivial_iff

added def Cycle.Nontrivial

added theorem Cycle.Subsingleton.congr

added theorem Cycle.Subsingleton.nodup

added def Cycle.Subsingleton

added theorem Cycle.card_to_multiset

added theorem Cycle.chain_coe_cons

added theorem Cycle.chain_iff_pairwise

added theorem Cycle.chain_map

added theorem Cycle.chain_ne_nil

added theorem Cycle.chain_of_pairwise

added theorem Cycle.chain_singleton

added theorem Cycle.coe_cons_eq_coe_append

added theorem Cycle.coe_eq_coe

added theorem Cycle.coe_eq_nil

added theorem Cycle.coe_nil

added theorem Cycle.coe_to_finset

added theorem Cycle.coe_to_multiset

added def Cycle.decidableNontrivialCoe

added theorem Cycle.empty_eq

added theorem Cycle.forall_eq_of_chain

added theorem Cycle.induction_on

added def Cycle.length

added theorem Cycle.length_coe

added theorem Cycle.length_nil

added theorem Cycle.length_nontrivial

added theorem Cycle.length_reverse

added theorem Cycle.length_subsingleton_iff

added def Cycle.lists

added theorem Cycle.lists_coe

added theorem Cycle.lists_nil

added def Cycle.map

added theorem Cycle.map_coe

added theorem Cycle.map_eq_nil

added theorem Cycle.map_nil

added theorem Cycle.mem_coe_iff

added theorem Cycle.mem_lists_iff_coe_eq

added theorem Cycle.mem_reverse_iff

added theorem Cycle.mk''_eq_coe

added theorem Cycle.mk_eq_coe

added theorem Cycle.next_reverse_eq_prev'

added theorem Cycle.next_reverse_eq_prev

added def Cycle.nil

added theorem Cycle.nil_to_finset

added theorem Cycle.nil_to_multiset

added theorem Cycle.nodup_coe_iff

added theorem Cycle.nodup_reverse_iff

added theorem Cycle.nontrivial_coe_nodup_iff

added theorem Cycle.nontrivial_reverse_iff

added theorem Cycle.not_mem_nil

added def Cycle.ofList

added theorem Cycle.prev_mem

added theorem Cycle.reverse_coe

added theorem Cycle.reverse_nil

added theorem Cycle.reverse_reverse

added theorem Cycle.subsingleton_nil

added theorem Cycle.subsingleton_reverse_iff

added def Cycle.toFinset

added theorem Cycle.toFinset_toMultiset

added def Cycle.toMultiset

added theorem Cycle.to_finset_eq_nil

added theorem Cycle.to_multiset_eq_nil

added def Cycle

added theorem List.isRotated_next_eq

added theorem List.isRotated_prev_eq

added theorem List.mem_of_nextOr_ne

added def List.next

added def List.nextOr

added theorem List.nextOr_concat

added theorem List.nextOr_cons_of_ne

added theorem List.nextOr_eq_nextOr_of_mem_of_ne

added theorem List.nextOr_mem

added theorem List.nextOr_nil

added theorem List.nextOr_self_cons_cons

added theorem List.nextOr_singleton

added theorem List.next_cons_concat

added theorem List.next_cons_cons_eq'

added theorem List.next_cons_cons_eq

added theorem List.next_get

added theorem List.next_getLast_cons

added theorem List.next_mem

added theorem List.next_ne_head_ne_getLast

added theorem List.next_nthLe

added theorem List.next_prev

added theorem List.next_reverse_eq_prev

added theorem List.next_singleton

added theorem List.pmap_next_eq_rotate_one

added theorem List.pmap_prev_eq_rotate_length_sub_one

added def List.prev

added theorem List.prev_cons_cons_eq'

added theorem List.prev_cons_cons_eq

added theorem List.prev_cons_cons_of_ne'

added theorem List.prev_cons_cons_of_ne

added theorem List.prev_getLast_cons'

added theorem List.prev_getLast_cons

added theorem List.prev_mem

added theorem List.prev_ne_cons_cons

added theorem List.prev_next

added theorem List.prev_nthLe

added theorem List.prev_reverse_eq_next

added theorem List.prev_singleton