coe_equivNatSum_apply_apply — Mathlib

English

For s ∈ Sym α n, the coefficient at a is the multiplicity of a in s.toMultiset: (equivNatSum α n s)(a) = (s : Multiset α).count a.

Русский

Для s ∈ Sym α n коэффициент при a равен количеству вхождений a в s.toMultiset.

LaTeX

$$$$ (\mathrm{equivNatSum}\ \alpha\ n\ s)(a) = (s : \operatorname{Multiset}\ \alpha).\text{count}(a). $$$$

Lean4

@[simp]
theorem coe_equivNatSum_apply_apply (s : Sym α n) (a : α) : (equivNatSum α n s : α →₀ ℕ) a = (s : Multiset α).count a :=
  rfl

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