Commit 2021-11-08 16:03 ef68f556

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.