Def Sym.equivNatSum

Modification history

2026-02-24 10:38

Mathlib/Data/Finsupp/Multiset.lean

chore: bump toolchain to v4.29.0-rc2 (#35708)

Deleted Sym.equivNatSum View on Github →

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