English
If f: Fin (m·n) → α, then List.ofFn f equals the flattening of List.ofFn (fun i : Fin n => List.ofFn (fun j : Fin m => f ⟨m·i + j, ...⟩)).
Русский
Если f: Fin(m·n) → α, то List.ofFn f равно расплющиванию List.ofFn (…);
LaTeX
$$$ \\operatorname{List.ofFn} f = \\operatorname{List.flatten} (\\operatorname{List.ofFn} (\\lambda i: \\mathrm{Fin} n, \\operatorname{List.ofFn} (\\lambda j: \\mathrm{Fin} m, f(\\langle m \\cdot i + j, \\cdots \\rangle)))) $$$
Lean4
/-- This breaks a list of `m*n` items into `n` groups each containing `m` elements. -/
theorem ofFn_mul' {m n} (f : Fin (m * n) → α) :
List.ofFn f =
List.flatten
(List.ofFn fun i : Fin n =>
List.ofFn fun j : Fin m =>
f
⟨m * i + j,
calc
m * i + j < m * (i + 1) := (Nat.add_lt_add_left j.prop _).trans_eq (by rw [Nat.mul_add, Nat.mul_one])
_ ≤ _ := Nat.mul_le_mul_left _ i.prop⟩) :=
by simp_rw [m.mul_comm, ofFn_mul, Fin.cast_mk]
