Commit 2021-12-06 14:45 81243140

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).