Commit 2021-02-16 18:36 35c070fa

View on Github →

chore(linear_algebra/dfinsupp): make lsum a linear_equiv (#6185) Zulip thread with a summary of the problem which required the nasty semimodule_of_linear_map present here.

Estimated changes

Modified src/linear_algebra/dfinsupp.lean

modified def dfinsupp.lsum

Modified src/linear_algebra/direct_sum_module.lean