Commit 2025-02-10 10:14 c335a815

feat(SkewMonoidAlgebra): coeff, single, one and sum (#19084)

feat : add definition of coeff, single, one and sum

In this PR, we introduce the notions of coeff, single, one and sum for skew monoid algebras.

Context

This is the second part of a planned series of PRs aiming to formalise skew monoid algebras. The PRs are split to ease the review process. The moral sum of these planned PRs is #10541 and the first part was #15878. After this PR, the goal will then be to finally define a skewed convolution product on SkewMonoidAlgebra k G. Here, the product of two elements f g : SkewMonoidAlgebra k G is the finitely supported function whose value at a is the sum of f x * (x • g y) over all pairs x, y such that x * y = a. (See #10541 at line 558 for an implementation.)