Theorems about Array.ofFn

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