Commit 2021-06-12 11:10 841dce13

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.