feat(data/{finsupp,dfinsupp}/basic): Scalar actions with zero

[YaelDillies]

Add a few scalar instances on finsupp and dfinsupp assuming smul_with_zero and stronger rather than distrib_mul_action.

---

• depends on: [Merged by Bors] - feat(group_theory/group_action): define distrib_smul and smul_zero_class #16123 to allow us to not duplicate those instances.

[eric-wieser]

Is it worth copying these to monoid_algebra, add_monoid_algebra, polynomial, and mv_polynomial?

[eric-wieser]

This all feels a bit unpleasant to me - either:

1. we care about smul_with_zero, and do want these instances. I really don't think we want to duplicate every single piece of the finsupp / dfinsupp smul API for it, and I think we should instead add the lower level typeclass you suggest
2. we don't care about smul_with_zero, and should just leave these instances missing
3. we care more about your smul_with_zero_on_one_side than we do the current smul_with_zero, and should just change the definition

I would lean towards option 2 for now, since adding yet another typeclass in the action hierarchy is hard to justify without motivating examples.

[adomani]

This is all happening at a level somewhat below the one where I am comfortable: I always try to stay away from explicitly working with finsupps and have learned to move around in polynomial, where the implementation is sufficiently hidden.

If this PR means that when I reach for simp to try to solve an finsupp.sum arising from a polynomial computation, it will simplify more, then I like this! Otherwise, I do not think that I have an opinion about these changes.

I am sorry if this review is vague, but as I said, I feel that I never would like to worry about finsupps, except that I suffer through them in polynomials!

[eric-wieser]

@adomani, can you remind us what the original motivation for smul_with_zero was? Specifically, for what X were you interested in smul_with_zero X M?

[adomani]

I originally wanted smul_with_zero for something coming from LTE. The specific issue was dealing with a vector space over the reals, and ℕ-submodules spanned by (finite) sets of vectors. The typeclass was supposed to make it easy to convert between multiplications by ℕ, ℤ, ℚ, ℝ on the same underlying vector space.

The idea was to combine this with the fact that multiplication by non-zero elements is injective (and hence the is_smul_regular definition as well).

Possibly, by now, there are better ways to deal with this?

[eric-wieser]

Maybe the simple answer is just "smul_with_zero exists such that mul_zero_class can be expressed with • too". I guess that was probably useful for linking regular and smul_regular.

That's enough to convince me that my option 3 above is a bad idea

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(group_theory/group_action): define distrib_smul and smul_zero_class #16123
  By Dependent Issues (🤖). Happy coding!

[YaelDillies]

A version of this made it to master.