nsmul_singleton — Mathlib

English

For any a ∈ α and n ∈ ℕ, n times the singleton {a} equals the multiset consisting of a repeated n times: n • {a} = replicate n a.

Русский

Для любого a ∈ α и n ∈ ℕ, n-кратно повторяем единичное множество {a} → результатreplicate n a.

LaTeX

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

Lean4

theorem nsmul_singleton (a : α) (n) : n • ({ a } : Multiset α) = replicate n a := by
  rw [← replicate_one, nsmul_replicate, mul_one]

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