Commit 2026-04-28 01:10 a45cae53

View on Github →

refactor(Algebra/MonoidAlgebra/PointwiseSMul): switch action from Finsupp to (Add)MonoidAlgebra and multiplicativize (#35243) This PR moves the API for convolution action on functions from Finsupp to MonoidAlgebra, adding a Semiring hypothesis. We do this move, because the convolution action of finsupps on formal functions is more naturally expressed as an action by the monoid algebra with its convolutional multiplication. This PR also multiplicativizes, preserving the original material with to_additive.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/MonoidAlgebra/PointwiseSMul.lean

added theorem MonoidAlgebra.mem_smulAntidiagonal_of_group

added theorem MonoidAlgebra.smul_apply_mulAction

added theorem MonoidAlgebra.smul_eq

Modified Mathlib/Data/Finset/SMulAntidiagonal.lean

modified theorem Finset.isPWO_support_smulAntidiagonal

modified theorem Finset.mem_smulAntidiagonal

modified theorem Finset.smulAntidiagonal_mono_left

modified theorem Finset.smulAntidiagonal_mono_right

modified theorem Finset.support_smulAntidiagonal_subset_smul

Modified Mathlib/Data/Finsupp/PointwiseSMul.lean

deleted theorem Finsupp.finite_vaddAntidiagonal

deleted theorem Finsupp.mem_vaddAntidiagonal_iff

deleted theorem Finsupp.mem_vaddAntidiagonal_of_addGroup

deleted theorem Finsupp.smul_apply_addAction

deleted theorem Finsupp.smul_eq

deleted def Finsupp.vaddAntidiagonal

Modified Mathlib/Data/Set/SMulAntidiagonal.lean

modified theorem Set.SMulAntidiagonal.eq_of_fst_eq_fst

modified theorem Set.SMulAntidiagonal.eq_of_snd_eq_snd

added theorem Set.SMulAntidiagonal.finite_of_finite_fst

modified theorem Set.SMulAntidiagonal.fst_eq_fst_iff_snd_eq_snd

Modified Mathlib/RingTheory/HahnSeries/Multiplication.lean

Modified Mathlib/RingTheory/HahnSeries/Summable.lean