mathlib

40acfb6a - chore(algebra/module/linear_map): move `map_sum` lemmas (#18106)

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_map`s 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.