Theorem Multiset.toFinsupp_sum_eq

Modification history

2024-03-14 11:12
Mathlib/Data/Finsupp/Multiset.lean
feat: the `n`th symmetric power is equivalent to maps of total mass `n`. (#11360)
Added Multiset.toFinsupp_sum_eqView on Github →