English
For any a in α, the map n ↦ replicate n a defines an additive monoid hom from (ℕ, +) to the multiset monoid Multiset α; in particular replicate 0 a is the empty multiset and replicate (n + m) a = replicate n a + replicate m a.
Русский
Для фиксированного a ∈ α отображение n ↦ replicate n a задаёт гомоморфизм моноида из (ℕ, +) в моноидMultiset α; в частности replicate 0 a — пустое мультимножество, и replicate (n + m) a = replicate n a + replicate m a.
LaTeX
$$$\exists \phi:\mathbb{N} \to^+ \mathrm{Multiset}(\alpha),\ \forall n\in\mathbb{N},\ \phi(n)=\mathrm{replicate}(n,a).$$$
Lean4
/-- `Multiset.replicate` as an `AddMonoidHom`. -/
@[simps]
def replicateAddMonoidHom (a : α) : ℕ →+ Multiset α
where
toFun n := replicate n a
map_zero' := replicate_zero a
map_add' _ _ := replicate_add _ _ a
