Commit 2023-01-20 16:27 55c79562

View on Github →

feat port data.vector.mem (#1697)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Vector/Mem.lean

added theorem Vector.get_mem

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_get

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