Commit 2023-01-09 07:05 40acfb6a

chore(algebra/module/linear_map): move map_sum lemmas (#18106) The lemmas linear_map.map_sum and linear_equiv.map_sum exist only for dot notation convenience, since linear_maps are of add_monoid_hom_class and therefore the generic lemma map_sum can replace them. Since these lemmas are the only reason that finsets are imported to algebra/module/linear_map, I propose deleting that import and moving the lemmas to linear_algebra/basic. This should open several files for porting.