Polynomial composition and map commute

Stream: maths

[Patrick Lutz]

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]

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]

can to_additive generate your map_sum from map_prod?

[Patrick Lutz]

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

[Thomas Browning]

do you just tag map_prod with to_additive?

[Jalex Stark]

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

[Scott Morrison]

@[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]

But yes, please PR polynomial.map_comp!

[Reid Barton]

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]

#3736