# Zulip Chat Archive

## 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