replicate_add — Mathlib

English

For all m,n and a, replicate(m+n, a) = replicate(m, a) ++ replicate(n, a).

Русский

Для любых m,n и a верно: replicate(m+n, a) = replicate(m, a) ++ replicate(n, a).

LaTeX

$$$$\\forall m\,\\forall n:\\\\mathbb{N},\\\\forall a:\\\\alpha, \\\\\\mathrm{replicate}(m+n, a) = \\\\\\mathrm{replicate}(m, a) \\\\\\append \\\\\\mathrm{replicate}(n, a).$$$$

Lean4

theorem replicate_add (m n) (a : α) : replicate (m + n) a = replicate m a ++ replicate n a := by
  rw [replicate_append_replicate]

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