mathlib3
8f78eb9c - feat(*): generalize to and add distrib_smul instances (#16132)

Commit
3 years ago
feat(*): generalize to and add distrib_smul instances (#16132) This PR builds on #16123 by adding `distrib_smul` (and `smul_zero_class`) instances for: * `finsupp` * `add_monoid_algebra` * `polynomial` * submodule quotients * scalar multiplication by `ℚ` It also generalizes some results by weakening `distrib_mul_action` to `distrib_smul`. The choice of instances and generalizations is based on which are necessary to solve instance diamonds in `splitting_field`, so I probably missed a lot of additional changes. Since I'm not so interested in generalizing everything at the moment, I'd rather leave missing instances to follow-up PRs. Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com>
Author
Parents
Loading