Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-27 23:02 c52b317f

View on Github →

refactor(data/finsupp): generalise finsupp.to_module (#284)

Estimated changes

Modified data/finsupp.lean

added theorem finsupp.smul_apply'

modified theorem finsupp.smul_apply

added def finsupp.to_has_scalar'

modified def finsupp.to_has_scalar

modified def finsupp.to_module

Modified data/polynomial.lean

Modified linear_algebra/basic.lean

Modified linear_algebra/multivariate_polynomial.lean