coe_countPAddMonoidHom — Mathlib

English

The canonical coercion of countPAddMonoidHom p to a function coincides with countP p; i.e., as functions Multiset α → ℕ, they are identical.

Русский

Коэрцированное отображение countPAddMonoidHom p на функцию совпадает с countP p; т.е. как функции Multiset α → ℕ они совпадают.

LaTeX

$$$(countPAddMonoidHom p : Multiset \alpha \to \mathbb{N}) = \operatorname{countP} p.$$$

Lean4

@[simp]
theorem coe_countPAddMonoidHom : (countPAddMonoidHom p : Multiset α → ℕ) = countP p :=
  rfl

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