mathlib

35c070fa - chore(linear_algebra/dfinsupp): make lsum a linear_equiv (#6185)

chore(linear_algebra/dfinsupp): make lsum a linear_equiv (#6185) [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Typeclass.20inference.20can't.20fill.20in.20parameters/near/226019081) with a summary of the problem which required the nasty `semimodule_of_linear_map` present here.