Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-13 15:24 71bb9f23

View on Github →

chore(linear_algebra/finsupp): Implement lsingle in terms of single_add_hom (#4605) While not shorter, this makes it easier to relate the two definitions

Estimated changes