Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finsupp.smul_apply'

Modification history

2021-02-26 10:06
src/data/finsupp/basic.lean
chore(data/finsupp/basic): add coe_{neg,sub,smul} lemmas to match coe_{zero,add,fn_sum} (#6350) …
Deleted finsupp.smul_apply'View on Github →
2020-10-18 01:46
src/data/finsupp/basic.lean
chore(data/finsupp/basic): rename type variables (#4624) …
Modified finsupp.smul_apply'View on Github →
2020-02-27 11:54
src/data/finsupp.lean
doc(data/finsupp): module docs and docstrings (#2059) …
Modified finsupp.smul_apply'View on Github →
2018-11-05 10:47
data/finsupp.lean
feat(linear_algebra,ring_theory): refactoring modules (#456) …
Modified finsupp.smul_apply'View on Github →
2018-08-27 23:02
data/finsupp.lean
refactor(data/finsupp): generalise finsupp.to_module (#284)
Added finsupp.smul_apply'View on Github →