Commit 2025-01-30 16:06 91155b5c

View on Github →

chore(Data/Finsupp/Basic): split SMul from file (#21230) This PR splits part of Data/Finsupp/Basic.lean related to SMul into a new SMul.lean file, addressing an instance of a long file linter trigger.

Estimated changes

deleted theorem Finsupp.comapDomain_smul
deleted def Finsupp.comapSMul
deleted theorem Finsupp.comapSMul_apply
deleted theorem Finsupp.comapSMul_def
deleted theorem Finsupp.comapSMul_single
deleted theorem Finsupp.filter_smul
deleted theorem Finsupp.mapDomain_smul
deleted theorem Finsupp.single_smul
deleted theorem Finsupp.smul_single'
deleted theorem Finsupp.smul_single_one
deleted theorem Finsupp.sum_smul_index'
deleted theorem Finsupp.sum_smul_index
deleted theorem Finsupp.support_smul_eq
deleted theorem IsSMulRegular.finsupp
added theorem Finsupp.comapSMul_def
added theorem Finsupp.filter_smul
added theorem Finsupp.mapDomain_smul
added theorem Finsupp.single_smul
added theorem Finsupp.smul_single'
added theorem Finsupp.sum_smul_index
added theorem IsSMulRegular.finsupp