Def Sym.equivNatSum

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