Commit 2022-07-18 22:20 f5d916a6

View on Github →

feat(data/vector/mem): Lemmas about membership in a vector (#15154) Add a number of lemmas about membership in different vectors. Some just wrap the list versions but some of the n+1 cases are more general.

Estimated changes

Modified src/data/vector/basic.lean

added theorem vector.eq_cons_iff

added theorem vector.exists_eq_cons

added theorem vector.head_map

deleted theorem vector.mem_iff_nth

added theorem vector.ne_cons_iff

deleted theorem vector.nth_mem

added theorem vector.tail_map

Created src/data/vector/mem.lean

added theorem vector.head_mem

added theorem vector.mem_cons_iff

added theorem vector.mem_cons_of_mem

added theorem vector.mem_cons_self

added theorem vector.mem_iff_nth

added theorem vector.mem_map_iff

added theorem vector.mem_map_succ_iff

added theorem vector.mem_of_mem_tail

added theorem vector.mem_succ_iff

added theorem vector.not_mem_map_zero

added theorem vector.not_mem_nil

added theorem vector.not_mem_zero

added theorem vector.nth_mem