ofFn_const — Mathlib

English

For any n and c, the list of constant c of length n is the replication of c, i.e., List.ofFn (fun _ : Fin n => c) = replicate n c.

Русский

Для любого n и c список, состоящий из повторяющегося c, равен replicate n c.

LaTeX

$$$ \\operatorname{List.ofFn} (\\lambda _ : \\mathrm{Fin} n, c) = \\operatorname{List.replicate} n\ c $$$

Lean4

@[simp]
theorem ofFn_const : ∀ (n : ℕ) (c : α), (ofFn fun _ : Fin n => c) = replicate n c
  | 0, c => by rw [ofFn_zero, replicate_zero]
  | n + 1, c => by rw [replicate, ← ofFn_const n]; simp

Похожие утверждения