Zulip Chat Archive

Stream: Is there code for X?

Topic: polynomial comp and map


view this post on Zulip Thomas Browning (Aug 10 2020 at 06:24):

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

view this post on Zulip Scott Morrison (Aug 10 2020 at 06:38):

I haven't seen that.

view this post on Zulip Scott Morrison (Aug 10 2020 at 06:38):

Presumably you should generalize it a bit before proving it.

view this post on Zulip Scott Morrison (Aug 10 2020 at 06:38):

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

view this post on Zulip Scott Morrison (Aug 10 2020 at 06:39):

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

view this post on Zulip Scott Morrison (Aug 10 2020 at 06:43):

It belongs in data/polynomial/eval.lean.

view this post on Zulip Thomas Browning (Aug 10 2020 at 06:45):

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


Last updated: May 17 2021 at 15:13 UTC