polynomial comp and map

Stream: Is there code for X?

[Thomas Browning]

I'm having trouble proving this lemma. Is this sort of thing in mathlib?

import field_theory.tower

lemma comp_map_lem (F : Type*) [field F] (f g : polynomial F) (E : Type*) [field E] [algebra F E] :
(f.comp(g)).map(algebra_map F E) = (f.map(algebra_map F E)).comp(g.map(algebra_map F E)) :=
begin
    sorry,
end

[Scott Morrison]

I haven't seen that.

[Scott Morrison]

Presumably you should generalize it a bit before proving it.

[Scott Morrison]

(i.e. to any ring_hom, not just for algebra_map)

[Scott Morrison]

(err.. maybe you need to keep some commutativity assumptions? I didn't think about it)

[Scott Morrison]

It belongs in data/polynomial/eval.lean.

[Thomas Browning]

yeah, that's the natural spot. I was looking for it there but I couldn't find it.