Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-02 22:24 dae87bcd

View on Github →

chore(data/finsupp/basic): Remove finsupp.leval which duplicates finsupp.lapply (#4876)

Estimated changes

Modified src/algebra/big_operators/finsupp.lean

Modified src/data/finsupp/basic.lean

added def finsupp.apply_add_hom

deleted theorem finsupp.coe_leval'

deleted theorem finsupp.coe_leval

deleted def finsupp.eval_add_hom

deleted theorem finsupp.eval_add_hom_apply

deleted def finsupp.leval'

deleted def finsupp.leval

Modified src/data/polynomial/coeff.lean

Modified src/linear_algebra/basis.lean

Modified src/linear_algebra/finsupp.lean