Commit 2025-05-12 11:42 4cb993ba

View on Github →

chore(Data/Finsupp/Defs): reduce imports (#24576) Move the algebra results to Algebra.Group.Finsupp

Estimated changes

added theorem Finsupp.add_apply
added theorem Finsupp.coe_add
added theorem Finsupp.coe_neg
added theorem Finsupp.coe_sub
added theorem Finsupp.embDomain_add
added theorem Finsupp.mapRange_add'
added theorem Finsupp.mapRange_add
added theorem Finsupp.mapRange_neg'
added theorem Finsupp.mapRange_neg
added theorem Finsupp.mapRange_sub'
added theorem Finsupp.mapRange_sub
added theorem Finsupp.neg_apply
added theorem Finsupp.sub_apply
added theorem Finsupp.support_add
added theorem Finsupp.support_add_eq
added theorem Finsupp.support_neg
added theorem Finsupp.support_sub
deleted theorem Finsupp.add_apply
deleted def Finsupp.applyAddHom
deleted theorem Finsupp.coe_add
deleted theorem Finsupp.coe_neg
deleted theorem Finsupp.coe_sub
deleted theorem Finsupp.embDomain_add
deleted theorem Finsupp.mapRange_add'
deleted theorem Finsupp.mapRange_add
deleted theorem Finsupp.mapRange_neg'
deleted theorem Finsupp.mapRange_neg
deleted theorem Finsupp.mapRange_sub'
deleted theorem Finsupp.mapRange_sub
deleted theorem Finsupp.neg_apply
deleted theorem Finsupp.sub_apply
deleted theorem Finsupp.support_add
deleted theorem Finsupp.support_add_eq
deleted theorem Finsupp.support_neg
deleted theorem Finsupp.support_sub