Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-28 15:03 31e5ae22

View on Github →

feat(data/list/cycle): Define the empty cycle (#12967) Also clean the file up somewhat, and add various simp lemmas.

Estimated changes

Modified src/data/list/cycle.lean

added theorem cycle.coe_eq_nil

added theorem cycle.coe_nil

added theorem cycle.coe_to_multiset

added theorem cycle.empty_eq

added theorem cycle.induction_on

modified theorem cycle.length_coe

added theorem cycle.length_nil

modified theorem cycle.length_nontrivial

modified theorem cycle.length_reverse

modified theorem cycle.length_subsingleton_iff

added theorem cycle.lists_coe

added theorem cycle.lists_nil

added theorem cycle.map_coe

added theorem cycle.map_eq_nil

added theorem cycle.map_nil

modified theorem cycle.mem_coe_iff

modified theorem cycle.mem_lists_iff_coe_eq

modified theorem cycle.mem_reverse_iff

modified theorem cycle.mk'_eq_coe

modified theorem cycle.mk_eq_coe

modified theorem cycle.next_mem

added def cycle.nil

added theorem cycle.nil_to_finset

added theorem cycle.nil_to_multiset

modified theorem cycle.nodup.nontrivial_iff

modified theorem cycle.nodup_coe_iff

added theorem cycle.nodup_nil

modified theorem cycle.nodup_reverse_iff

modified theorem cycle.nontrivial_reverse_iff

added theorem cycle.not_mem_nil

modified theorem cycle.prev_mem

modified theorem cycle.reverse_coe

added theorem cycle.reverse_nil

modified theorem cycle.reverse_reverse

modified theorem cycle.subsingleton.nodup

added theorem cycle.subsingleton_nil

modified theorem cycle.subsingleton_reverse_iff