Zulip Chat Archive

Stream: maths

Topic: Polynomial composition and map commute


view this post on Zulip Patrick Lutz (Aug 10 2020 at 20:57):

For the Berkeley Galois theory project, we had to use the following fact: if ff and gg are polynomials over a ring RR and ι\iota is a map from RR to a ring SS then ι(f(g))=(ι(f))(ι(g))\iota(f(g)) = (\iota(f))(\iota(g)). We couldn't find this fact in mathlib, so we proved it here. Is it really true that this is not in mathlib? If not, then I will make a PR to add it.

view this post on Zulip Patrick Lutz (Aug 10 2020 at 20:59):

Also, is this lemma already in mathlib? It's almost exactly the same as polynomial.map_prod but for sums instead of products.

view this post on Zulip Jalex Stark (Aug 10 2020 at 21:56):

can to_additive generate your map_sum from map_prod?

view this post on Zulip Patrick Lutz (Aug 10 2020 at 22:06):

I don't know how to_additive works. Is there somewhere I can read about it or see examples?

view this post on Zulip Thomas Browning (Aug 10 2020 at 22:07):

do you just tag map_prod with to_additive?

view this post on Zulip Jalex Stark (Aug 10 2020 at 22:13):

searching to_additive in github shows examples:
https://github.com/leanprover-community/mathlib/search?q=to_additive&unscoped_q=to_additive

view this post on Zulip Scott Morrison (Aug 11 2020 at 00:33):

@[to_additive] probably starts to become unreliable in the polynomial world. When both multiplicative and additive structures are simultaneously present (...pretty much the definition of talking about polynomials...) it often requires more hand-holding than is worth it.

view this post on Zulip Scott Morrison (Aug 11 2020 at 00:33):

But yes, please PR polynomial.map_comp!

view this post on Zulip Reid Barton (Aug 11 2020 at 00:46):

My initial reaction was that it wouldn't work (because addition and multiplication of polynomials are totally different things) but if it works by just making certain textual changes to the statement of the proof of the lemma then I guess it might actually work in this case after all.

view this post on Zulip Patrick Lutz (Aug 11 2020 at 03:45):

#3736


Last updated: May 10 2021 at 07:15 UTC