## Stream: maths

### Topic: polynomial.map

#### Kevin Buzzard (Oct 14 2020 at 18:06):

polynomial.map has type (R →+* S) → polynomial R → polynomial S. Is there any reason this is not a semiring hom? I was trying to remove a deprecated import; the issue is map.is_semiring_hom, the "old-fashioned" proof (i.e. just what we need to make the semiring hom). I don't know my way around polynomials, I just know it's moved fast recently. Do people really use this map? I don't know how to search for it. Searching directly for polynomial.map finds only four uses in mathlib, but I'm aware there could be more.

#### Yury G. Kudryashov (Oct 14 2020 at 19:03):

BTW, it would be nice to have it for any monoid_algebra.

#### Eric Wieser (Oct 14 2020 at 21:06):

I think I have this for monoid_algebra in #4321

#### Eric Wieser (Oct 15 2020 at 11:43):

Thanks for the inspiration of looking in polynomial for proofs I want in monoid_algebra - it led to a bunch of golfing in #4627

Last updated: May 12 2021 at 08:14 UTC