Commit 2022-03-09 05:46 94e9bb55

View on Github →

chore(data/{finsupp,dfinsupp}/basic): use the injective APIs (#12534) This also fixes a scalar diamond in the nat and int actions on dfinsupp. The diamond did not exist for finsupp.

Estimated changes

Modified src/data/dfinsupp/basic.lean

added theorem dfinsupp.coe_nsmul

added theorem dfinsupp.coe_zsmul

added theorem dfinsupp.nsmul_apply

added theorem dfinsupp.zsmul_apply

Modified src/data/finsupp/basic.lean

Modified src/data/finsupp/pointwise.lean