Mathlib v3 is deprecated. Go to Mathlib v4

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