Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-16 12:05 8d9eb266

View on Github →

chore(linear_algebra/finsupp): make lsum a linear_equiv (#6183)

Estimated changes

modified theorem finsupp.coe_lsum
modified def finsupp.lsum
modified theorem finsupp.lsum_symm_apply