English
For a : Fin m → α and n ∈ ℕ, List.ofFn (Fin.repeat n a) equals (List.replicate n (List.ofFn a)).flatten.
Русский
Для a: Fin m → α и n≥0, List.ofFn (Fin.repeat n a) = (List.replicate n (List.ofFn a)).flatten.
LaTeX
$$$ \\operatorname{List.ofFn}(\\operatorname{Fin.repeat} n\ a) = (\\operatorname{List.replicate} n (\\operatorname{List.ofFn} a)).\\text{flatten} $$$
Lean4
@[simp]
theorem ofFn_fin_repeat {m} (a : Fin m → α) (n : ℕ) :
List.ofFn (Fin.repeat n a) = (List.replicate n (List.ofFn a)).flatten := by
simp_rw [ofFn_mul, ← ofFn_const, Fin.repeat, Fin.modNat, Nat.add_comm, Nat.add_mul_mod_self_right,
Nat.mod_eq_of_lt (Fin.is_lt _)]
