Commit 2025-08-07 13:48 482cd792

View on Github →

chore: move algebraic properties of Finsupp.single to Algebra.Group.Finsupp (#28073) They do not belong under Data as they are not about a datatype.

Estimated changes

added theorem Finsupp.apply_single
added theorem Finsupp.erase_add
added theorem Finsupp.erase_neg
added theorem Finsupp.erase_sub
added theorem Finsupp.induction₂
modified theorem Finsupp.mapRange_neg'
modified theorem Finsupp.mapRange_sub'
added theorem Finsupp.single_add
added theorem Finsupp.single_neg
added theorem Finsupp.single_sub
modified theorem Finsupp.support_neg
modified theorem Finsupp.support_sub
deleted theorem Finsupp.apply_single
deleted def Finsupp.eraseAddHom
deleted theorem Finsupp.erase_add
deleted theorem Finsupp.erase_add_single
deleted theorem Finsupp.erase_neg
deleted theorem Finsupp.erase_sub
deleted theorem Finsupp.induction_linear
deleted theorem Finsupp.induction_on_max
deleted theorem Finsupp.induction_on_min
deleted theorem Finsupp.induction₂
deleted theorem Finsupp.single_add
deleted theorem Finsupp.single_add_apply
deleted theorem Finsupp.single_add_erase
deleted theorem Finsupp.single_neg
deleted theorem Finsupp.single_sub