Theorems about Array.ofFn

@[simp]

theorem Array.ofFn_zero {α : Type u_1} {f : Fin 0 → α} : ofFn f = #[]

theorem Array.ofFn_succ {n : Nat} {α : Type u_1} {f : Fin (n + 1) → α} : ofFn f = (ofFn fun (i : Fin n) => f i.castSucc).push (f ⟨n, ⋯⟩)

@[simp]

theorem List.toArray_ofFn {n : Nat} {α : Type u_1} {f : Fin n → α} : (ofFn f).toArray = Array.ofFn f

@[simp]

theorem Array.toList_ofFn {n : Nat} {α : Type u_1} {f : Fin n → α} : (ofFn f).toList = List.ofFn f

@[simp]

theorem Array.ofFn_eq_empty_iff {n : Nat} {α : Type u_1} {f : Fin n → α} : ofFn f = #[] ↔ n = 0

@[simp]

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