Theorems · Theorem

List.ofFn_mul

∀ {α : Type u} {m n : ℕ} (f : Fin (m * n) → α),
  List.ofFn f = (List.ofFn fun i => List.ofFn fun j => f ⟨↑i * n + ↑j, ⋯⟩).flatten

This breaks a list of m*n items into m groups each containing n elements.

Defined in

Mathlib.Data.List.OfFn

Cited by

2 results in Mathlib

Foundations

Depth 49 from the axioms · uses propext, Quot.sound