theorem Vector.toArray_injective {α : Type u_1} {n : Nat} {v w : Vector α n} : v.toArray = w.toArray → v = w

mk lemmas

@[simp]

theorem Vector.get_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Fin n) : { toArray := a, size_toArray := h }.get i = a[i]

@[simp]

theorem Vector.getD_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (x : α) : { toArray := a, size_toArray := h }.getD i x = a.getD i x

@[simp]

theorem Vector.uget_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : USize) (hi : i.toNat < n) : { toArray := a, size_toArray := h }.uget i hi = a.uget i ⋯

tail lemmas

theorem Vector.tail_eq_of_zero {α : Type u_1} {v : Vector α 0} : v.tail = { toArray := #[], size_toArray := ⋯ }

theorem Vector.tail_eq_of_ne_zero {n : Nat} {α : Type u_1} [NeZero n] {v : Vector α n} : v.tail = v.eraseIdx 0 ⋯

theorem Vector.toList_tail {α : Type u_1} {n : Nat} {v : Vector α n} : v.tail.toList = v.toList.tail

getElem lemmas

theorem Vector.getElem_tail {α : Type u_1} {n : Nat} {v : Vector α n} {i : Nat} (hi : i < n - 1) : v.tail[i] = v[i + 1]

get lemmas

@[simp]

theorem Vector.get_push_last {α : Type u_1} {n : Nat} (v : Vector α n) (a : α) : (v.push a).get (Fin.last n) = a

@[simp]

theorem Vector.get_push_castSucc {α : Type u_1} {n : Nat} (v : Vector α n) (a : α) (i : Fin n) : (v.push a).get i.castSucc = v.get i

@[simp]

theorem Vector.get_map {α : Type u_1} {n : Nat} {β : Type u_2} (v : Vector α n) (f : α → β) (i : Fin n) : (map f v).get i = f (v.get i)

@[simp]

theorem Vector.get_reverse {α : Type u_1} {n : Nat} (v : Vector α n) (i : Fin n) : v.reverse.get i = v.get i.rev

@[simp]

theorem Vector.get_replicate {α : Type u_1} (n : Nat) (a : α) (i : Fin n) : (replicate n a).get i = a

@[simp]

theorem Vector.get_range (n : Nat) (i : Fin n) : (range n).get i = ↑i

@[simp]

theorem Vector.get_ofFn {n : Nat} {α : Type u_1} (f : Fin n → α) (i : Fin n) : (ofFn f).get i = f i

@[simp]

theorem Vector.get_cast {α : Type u_1} {m n : Nat} (v : Vector α m) (h : m = n) (i : Fin n) : (Vector.cast h v).get i = v.get (Fin.cast ⋯ i)

theorem Vector.get_tail {α : Type u_1} {n : Nat} (v : Vector α (n + 1)) (i : Fin n) : v.tail.get i = v.get i.succ