map_replicate — Mathlib

English

The map of a replicated element is the replication of the mapped element: map f (replicate k a) = replicate k (f a).

Русский

Отображение f распределяет повторения: map f (replicate k a) = replicate k (f a).

LaTeX

$$$$ \\mathrm{map} f (\\mathrm{replicate} k\\ a) = \\mathrm{replicate} k (f\\ a) $$$$

Lean4

@[simp]
theorem map_replicate (f : α → β) (k : ℕ) (a : α) : (replicate k a).map f = replicate k (f a) := by
  simp only [← coe_replicate, map_coe, List.map_replicate]

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