Theorems about List.ofFn

@[simp]

theorem List.length_ofFn {n : Nat} {α : Type u_1} (f : Fin n → α) : (List.ofFn f).length = n

@[simp]

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

@[simp]

theorem List.getElem?_ofFn {n : Nat} {α : Type u_1} (f : Fin n → α) (i : Nat) : (List.ofFn f)[i]? = List.ofFnNthVal f i

@[simp]

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