Theorem Sym.coe_equivNatSum_apply_apply

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 Sym.coe_equivNatSum_apply_applyView on Github →