mathlib3

841dce13 - feat(data/polynomial): generalize `polynomial.has_scalar` to require only `distrib_mul_action` instead of `semimodule` (#7664)

feat(data/polynomial): generalize `polynomial.has_scalar` to require only `distrib_mul_action` instead of `semimodule` (#7664) Note that by generalizing this instance, we introduce a diamond with `polynomial.mul_semiring_action`, which has a definitionally different `smul`. To resolve this, we add a proof that the definitions are equivalent, and switch `polynomial.mul_semiring_action` to use the same implementation as `polynomial.has_scalar`. This allows us to generalize `smul_C` to apply to all types of action, and remove `coeff_smul'` which then duplicates the statement of `coeff_smul`.