# Zulip Chat Archive

## Stream: maths

### Topic: Polynomial composition and map commute

#### Patrick Lutz (Aug 10 2020 at 20:57):

For the Berkeley Galois theory project, we had to use the following fact: if $f$ and $g$ are polynomials over a ring $R$ and $\iota$ is a map from $R$ to a ring $S$ then $\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.

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

#### Jalex Stark (Aug 10 2020 at 21:56):

can `to_additive`

generate your `map_sum`

from `map_prod`

?

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

#### Thomas Browning (Aug 10 2020 at 22:07):

do you just tag map_prod with to_additive?

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

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

#### Scott Morrison (Aug 11 2020 at 00:33):

But yes, please PR `polynomial.map_comp`

!

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

#### Patrick Lutz (Aug 11 2020 at 03:45):

Last updated: May 10 2021 at 07:15 UTC