English
If f: Fin (m·n) → α, then List.ofFn f equals the flattening of a two-level list: List.ofFn fun i: Fin m => List.ofFn (fun j: Fin n => f ⟨i·n + j, proof⟩).
Русский
Если f: Fin(m·n) → α, то List.ofFn f равно расплющиванию двухуровневого списка: List.ofFn (Fin.append ...).
LaTeX
$$$ \\operatorname{List.ofFn} f = \\operatorname{List.flatten} (\\operatorname{List.ofFn} (\\lambda i: \\mathrm{Fin}\, m, \\operatorname{List.ofFn} (\\lambda j: \\mathrm{Fin}\, n, f(\\langle i \\cdot n + j, \\cdots \\rangle)))) $$$
Lean4
/-- This breaks a list of `m*n` items into `m` groups each containing `n` elements. -/
theorem ofFn_mul {m n} (f : Fin (m * n) → α) :
List.ofFn f =
List.flatten
(List.ofFn fun i : Fin m =>
List.ofFn fun j : Fin n =>
f
⟨i * n + j,
calc
↑i * n + j < (i + 1) * n := (Nat.add_lt_add_left j.prop _).trans_eq (by rw [Nat.add_mul, Nat.one_mul])
_ ≤ _ := Nat.mul_le_mul_right _ i.prop⟩) :=
by
induction m with
| zero => simp [ofFn_zero, Nat.zero_mul, ofFn_zero]
| succ m IH =>
simp_rw [ofFn_succ', succ_mul]
simp [ofFn_add, IH]
rfl
