Theorems about Vector.ofFn

@[simp]

theorem Vector.getElem_ofFn {i : Nat} {α : Type u_1} {n : Nat} {f : Fin n → α} (h : i < n) : (ofFn f)[i] = f ⟨i, h⟩

theorem Vector.getElem?_ofFn {i : Nat} {α : Type u_1} {n : Nat} {f : Fin n → α} : (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none

@[simp]

theorem Vector.mem_ofFn {α : Type u_1} {n : Nat} {f : Fin n → α} {a : α} : a ∈ ofFn f ↔ ∃ (i : Fin n), f i = a

theorem Vector.back_ofFn {α : Type u_1} {n : Nat} [NeZero n] {f : Fin n → α} : (ofFn f).back = f ⟨n - 1, ⋯⟩