[Merged by Bors] - feat: algebraic properties of LinearMap.compMultilinear

[eric-wieser]

This also demotes LinearMap.compAlternatingMap to a plain function, for consistency.

To make up for this loss, it introduces LinearMap.compAlternatingMapₗ as the stronger linear version.

---

[github-actions]

PR summary a644005b86

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ _root_.LinearMap.compMultilinearMapₗ
+ add_compAlternatingMap
+ add_compMultilinearMap
+ compAlternatingMap_add
+ compAlternatingMap_smul
+ compAlternatingMap_zero
+ compAlternatingMapₗ
+ compMultilinearMap_add
+ compMultilinearMap_smul
+ compMultilinearMap_zero
+ smul_compAlternatingMap
+ smul_compMultilinearMap
+ zero_compAlternatingMap
+ zero_compMultilinearMap

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.

[urkud]

We have several different conventions about naming of bundled versions of maps. Some day, we should decide what to do about it.

[eric-wieser]

In this case, I copied MultilinearMap.compLinearMapₗ

[urkud]

Thanks! 🎉
bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style