mathlib3

ef68f556 - feat(linear_algebra/multilinear/basis): multilinear maps on basis vectors (#10090)

feat(linear_algebra/multilinear/basis): multilinear maps on basis vectors (#10090) Add two versions of the fact that a multilinear map on finitely many arguments is determined by its values on basis vectors. The precise requirements for each version follow from the results used in the proof: `basis.ext_multilinear_fin` uses the `curry` and `uncurry` results to deduce it from `basis.ext` and thus works for multilinear maps on a family of modules indexed by `fin n`, while `basis.ext_multilinear` works for an arbitrary `fintype` index type but is limited to the case where the modules for all the arguments (and the bases used for those modules) are the same, since it's derived from the previous result using `dom_dom_congr` which only handles the case where all the modules are the same. This is in preparation for proving a corresponding result for alternating maps, for which the case of all argument modules the same suffices. There is probably room for making results more general.