coe_equivNatSumOfFintype_symm_apply

English

For [Fintype α], ((equivNatSumOfFintype α n).symm P : Multiset α) = ∑ a, P(a) • {a}.

Русский

Для [Fintype α] выполняется: ((equivNatSumOfFintype α n).symm P : Multiset α) = \sum_a P(a) \cdot {a}.

LaTeX

$$$$ ((\mathrm{equivNatSumOfFintype}\ \alpha\ n).symm P : \operatorname{Multiset} \alpha) = \sum_{a} P(a) \cdot \{a\}. $$$$

Lean4

@[simp]
theorem coe_equivNatSumOfFintype_symm_apply [Fintype α] (P : { P : α → ℕ // ∑ i, P i = n }) :
    ((equivNatSumOfFintype α n).symm P : Multiset α) = ∑ a, ((P : α → ℕ) a) • { a } :=
  by
  obtain ⟨P, hP⟩ := P
  change Finsupp.toMultiset (Finsupp.equivFunOnFinite.symm P) = Multiset.sum _
  ext a
  rw [Multiset.count_sum]
  simp [Multiset.count_singleton]

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