Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-12 01:24 8c887216

View on Github →

feat(data/list): assorted lemmas (#2651) Some lemmas I found useful for #2578

Estimated changes

added theorem list.cons_head'_tail
added theorem list.head_mem_head'
added theorem list.ilast_eq_last'
added theorem list.init_append_last'
added theorem list.is_nil_iff_eq_nil
added theorem list.last'_append_cons
added theorem list.last'_is_none
added theorem list.last'_is_some
modified theorem list.last_cons
added theorem list.last_mem
added theorem list.mem_last'_eq_last
added theorem list.mem_of_mem_head'
added theorem list.mem_of_mem_last'
added theorem list.prod_eq_foldr
added theorem list.chain'.append
added theorem list.chain'.cons'
added theorem list.chain'.imp_head
added theorem list.chain'.rel_head'
added theorem list.chain'.rel_head
added theorem list.chain'_cons'