coe_equivNatSum_symm_apply — Mathlib

English

The inverse of the NatSum equivalence sends P to a multiset obtained by P, i.e., ((equivNatSum α n).symm P : Multiset α) = toMultiset(P).

Русский

Обратное NatSum эквивалентности восстанавливает мультимножество по P: ((equivNatSum α n).symm P : Multiset α) = toMultiset(P).

LaTeX

$$$$ ((\mathrm{equivNatSum}\ \alpha\ n).symm P : \operatorname{Multiset} \alpha) = \mathrm{toMultiset}(P). $$$$

Lean4

@[simp]
theorem coe_equivNatSum_symm_apply (P : { P : α →₀ ℕ // P.sum (fun _ ↦ id) = n }) :
    ((equivNatSum α n).symm P : Multiset α) = Finsupp.toMultiset P :=
  rfl

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