feat: add `MultilinearMap.dfinsuppFamily` and `MultilinearMap.piFamily`

[eric-wieser]

This is the analog to Fintype.piFinset

Since this is computable and rather confusing, I've included a test with a concrete evaluation.

---

• [x] depends on: #17882 (for the test)

[github-actions[bot]]

PR summary 44c1065481

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.LinearAlgebra.Multilinear.Pi	730
Mathlib.LinearAlgebra.Multilinear.DFinsupp	862

---

Declarations diff

+ dfinsuppFamily + dfinsuppFamily_add + dfinsuppFamily_compLinearMap_lsingle + dfinsuppFamily_single + dfinsuppFamily_smul + dfinsuppFamily_zero + dfinsuppFamilyₗ + piFamily + piFamily_add + piFamily_compLinearMap_lsingle + piFamily_single + piFamily_smul + piFamily_zero + piFamilyₗ + support_dfinsuppFamily_subset

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>

The doc-module for script/declarations_diff.sh contains some details about this script.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#17882~~ By Dependent Issues (🤖). Happy coding!

[jcommelin]

bors d+

[mathlib-bors[bot]]

:v: eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[eric-wieser]

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style