coeff): generalize polynomial.coeff_smul to match mv_polynomial.coeff_smul (#7663)

Commit

4 years ago

feat(data/polynomial/coeff): generalize polynomial.coeff_smul to match mv_polynomial.coeff_smul (#7663) Notably this means these lemmas cover `nat` and `int` actions.

Author

eric-wieser

Parents

599712ff

mathlib ed4161c5 - feat(data/polynomial/coeff): generalize polynomial.coeff_smul to match mv_polynomial.coeff_smul (#7663)

mathlib
ed4161c5 - feat(data/polynomial/coeff): generalize polynomial.coeff_smul to match mv_polynomial.coeff_smul (#7663)