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) : (mk a h).get i = a[i]

@[simp]

theorem Vector.getD_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (x : α) : (mk a 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) : (mk a h).uget i hi = a.uget i ⋯

tail lemmas

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

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

theorem Vector.get_eq_getElem {α : Type u_1} {n : Nat} (v : Vector α n) (i : Fin n) : v.get i = v[↑i]

@[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

finIdxOf? lemmas

@[simp]

theorem Vector.finIdxOf?_empty {α : Type u_1} {a : α} [BEq α] (v : Vector α 0) : v.finIdxOf? a = none

@[simp]

theorem Vector.finIdxOf?_eq_none_iff {α : Type u_1} {n : Nat} [BEq α] [LawfulBEq α] {v : Vector α n} {a : α} : v.finIdxOf? a = none ↔ ¬a ∈ v

@[simp]

theorem Vector.finIdxOf?_eq_some_iff {α : Type u_1} {n : Nat} [BEq α] [LawfulBEq α] {v : Vector α n} {a : α} {i : Fin n} : v.finIdxOf? a = some i ↔ v.get i = a ∧ ∀ (j : Fin n), j < i → ¬v.get j = a

@[simp]

theorem Vector.isSome_finIdxOf? {α : Type u_1} {n : Nat} [BEq α] [PartialEquivBEq α] {v : Vector α n} {a : α} : (v.finIdxOf? a).isSome = v.contains a

@[simp]

theorem Vector.isNone_finIdxOf? {α : Type u_1} {n : Nat} [BEq α] [PartialEquivBEq α] {v : Vector α n} {a : α} : (v.finIdxOf? a).isNone = !v.contains a