Row-major finite arrays as lists

Main results

• List.flatMap_ofFn_prod: nested row-major enumeration agrees with the existing product equivalence on finite indices.
• List.getD_flatMap_ofFn: read a cell at its ordinary flat row-major index.

theorem List.flatMap_ofFn_prod {α : Type u_1} {n d : ℕ} (f : Fin n → Fin d → α) : flatMap (fun (i : Fin n) => ofFn (f i)) (finRange n) = ofFn fun (p : Fin (n * d)) => f (finProdFinEquiv.symm p).1 (finProdFinEquiv.symm p).2

Flattening all rows enumerates the standard finite product equivalence.

theorem List.getD_flatMap_ofFn {α : Type u_1} {n d : ℕ} (f : Fin n → Fin d → α) (default : α) (i : Fin n) (j : Fin d) : (flatMap (fun (i : Fin n) => ofFn (f i)) (finRange n)).getD (↑i * d + ↑j) default = f i j

Ordinary flat indexing reads the corresponding original row and column.