Commit 2023-01-29 02:02 ecfe8d5a

View on Github →

feat: port Data.Finsupp.Pointwise (#1917)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finsupp/Pointwise.lean

added theorem Finsupp.coe_mul

added theorem Finsupp.coe_pointwise_smul

added theorem Finsupp.mul_apply

added theorem Finsupp.support_mul