[Merged by Bors] - feat: Create a partition from an element of Sym

[SashaIr]

An element of Sym induces a partition given by the multiplicities of its elements.

Co-authored-by: Nirvana Coppola [email protected]

---

See #12572.

[github-actions]

PR summary 021afbfb95

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ ofSym
+ ofSymShapeEquiv
+ ofSym_map
+ ofSym_one
+ oneEquiv

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style