Commit 2025-07-24 14:37 615d661c

View on Github →

chore: generalize typeclass assumptions on DFinsupp SMul (#27409) These match the Finsupp instances more closely.

Estimated changes

Modified Mathlib/Data/DFinsupp/Module.lean

modified theorem DFinsupp.coe_smul

modified theorem DFinsupp.comapDomain'_smul

modified theorem DFinsupp.comapDomain_smul

modified theorem DFinsupp.equivProdDFinsupp_smul

modified theorem DFinsupp.filter_smul

modified theorem DFinsupp.smul_apply

modified theorem DFinsupp.subtypeDomain_smul

modified theorem DFinsupp.support_smul