[Merged by Bors] - feat(data/polynomial/coeff): Add smul_eq_C_mul

[BoltonBailey]

Adding a lemma polynomial.smul_eq_C_mul for single variate polynomials analogous to mv_polynomial.smul_eq_C_mul for multivariate.

---

[eric-wieser]

Lemma name and statement seems good, as it matches mv_polynomial

Any particular reason for putting in at this file? data.polynomial.monomial might be a better place.

[BoltonBailey]

I initially wanted to put it in data.polynomial.monomial but my proof relies on lemmas from this file, and to import this file into data.polynomial.monomial would be a circular import. Seems like a similar thing has happened with C_mul_X_pow_eq_monomial which feels more appropriate in monomial but has ended up here.

[BoltonBailey]

It seems coeff imports monomial to use the C function and, single_eq_C_mul_X and monomial_eq_smul_X lemmas defined there, but it's not clear to me why C should be in the monomial file anyway. I would propose a refactor where C and the lemmas about it are moved to basic.lean, and the import is switched so that monomial imports coeff.

[eric-wieser]

Another option is just to move polynomial.algebra_of_algebra to polynomial.basic (it's a one-line declaration!), and then smul_eq_C_mul can be proven by just algebra.smul_def

[BoltonBailey]

In the algebra_map definition of algebra_of_algebra, R is a comm_semiring. Whereas in the current version of this pull request, R does not have to be commutative.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests