mathlib

81243140 - feat(linear_algebra/multilinear/basic,linear_algebra/alternating): comp_linear_map lemmas (#10631)

feat(linear_algebra/multilinear/basic,linear_algebra/alternating): comp_linear_map lemmas (#10631) Add more lemmas about composing multilinear and alternating maps with linear maps in each argument. Where I wanted a lemma for either of multilinear or alternating maps, I added it for both. There are however some lemmas for `alternating_map.comp_linear_map` that don't have equivalents at present for `multilinear_map.comp_linear_map` (I added one such equivalent `multilinear_map.zero_comp_linear_map` because I needed it for another lemma, but didn't try adding such equivalents of existing lemmas where I didn't need them).