nsmul_replicate — Mathlib

English

For any a ∈ α and n,m ∈ ℕ, n times replicating m copies of a equals replicating n·m copies of a: n · replicate m a = replicate (n·m) a.

Русский

Для любого a ∈ α и n,m ∈ ℕ n-кратно повторяем m копий элемента a дает replicate (n·m) копий a: n · replicate m a = replicate (n·m) a.

LaTeX

$$$n \cdot \mathrm{replicate}(m,a) = \mathrm{replicate}(n\cdot m,a).$$$

Lean4

theorem nsmul_replicate {a : α} (n m : ℕ) : n • replicate m a = replicate (n * m) a :=
  ((replicateAddMonoidHom a).map_nsmul _ _).symm

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