polynomial.map

Stream: maths

[Kevin Buzzard]

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]

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

[Eric Wieser]

I think I have this for monoid_algebra in #4321

[Eric Wieser]

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