Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-13 17:34 ea197760

View on Github →

refactor(data/finsupp): generalize module construction for finsupp

Estimated changes

Modified algebra/linear_algebra/basic.lean

deleted theorem lc.smul_apply

deleted theorem lc.sum_smul_index

Modified algebra/linear_algebra/multivariate_polynomial.lean

Modified data/finsupp.lean

modified theorem finsupp.neg_apply

modified def finsupp.prod

modified theorem finsupp.prod_map_range_index

modified theorem finsupp.prod_neg_index

modified theorem finsupp.prod_single_index

modified theorem finsupp.prod_zero_index

added theorem finsupp.smul_apply

modified theorem finsupp.sub_apply

modified def finsupp.sum

added theorem finsupp.sum_smul_index

added def finsupp.to_has_scalar

added def finsupp.to_module