countAddMonoidHom — Mathlib

English

For a fixed a ∈ α, the function countAddMonoidHom a : Multiset α →+ ℕ is the AddMonoidHom given by s ↦ count a s, i.e., the multiplicity of a in s.

Русский

Для фиксированного a ∈ α функция countAddMonoidHom a : Multiset α →+ ℕ задаёт гомоморфизм AddMonoid ... отображение s ↦ count a s, т.е. кратность a в s.

LaTeX

$$$\text{countAddMonoidHom } a: \mathrm{Multiset}(\alpha) \to^+ \mathbb{N},\ \text{где } (\text{toFun})(s) = \operatorname{count}(a,s).$$$

Lean4

/-- `count a`, the multiplicity of `a` in a multiset, promoted to an `AddMonoidHom`. -/
def countAddMonoidHom (a : α) : Multiset α →+ ℕ :=
  countPAddMonoidHom (a = ·)

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