Zulip Chat Archive

Stream: maths

Topic: polynomial.map


view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Oct 14 2020 at 19:03):

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

view this post on Zulip Eric Wieser (Oct 14 2020 at 21:06):

I think I have this for monoid_algebra in #4321

view this post on Zulip 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