Zulip Chat Archive

Stream: Is there code for X?

Topic: polynomial.eval_eval₂

Kevin Buzzard (Dec 19 2021 at 23:43):

Do we have this?

import tactic
import data.polynomial.eval

open polynomial

variables {R S T : Type*} [semiring R] [semiring S] [semiring T] (f : R →+* S) (g : S →+* T)

lemma polynomial.eval_eval₂ (p : polynomial R) (s : S) : g (eval₂ f s p) = eval₂ (g.comp f) (g s) p :=
begin
  sorry,
end

We have polynomial.eval₂_comp but it's composing p's not f's.

Eric Rodriguez (Dec 20 2021 at 00:16):

docs#polynomial.hom_eval₂

Eric Rodriguez (Dec 20 2021 at 00:17):

come on linkifier...

Eric Rodriguez (Dec 20 2021 at 00:17):

https://leanprover-community.github.io/mathlib_docs/data/polynomial/eval.html#polynomial.hom_eval%E2%82%82

Thomas Browning (Dec 20 2021 at 00:20):

rw [←eval₂_map, eval₂_at_apply, eval_map],

Eric Rodriguez (Dec 20 2021 at 00:24):

want to PR that golf Thomas? the current proof is ridiculous ;b

Thomas Browning (Dec 20 2021 at 00:26):

Already on it!

Thomas Browning (Dec 20 2021 at 00:29):

#10920

Kevin Buzzard (Dec 20 2021 at 00:49):

What? Why did library_search not find it for me?

Thomas Browning (Dec 20 2021 at 00:50):

Maybe because the mathlib version currently assumes comm_semiring?

Kevin Buzzard (Dec 20 2021 at 00:51):

Oh I'm apparently missing comm_ assumptions. Thanks!

Thomas Browning (Dec 20 2021 at 01:02):

(but notice the new proof in #10920 drops the comm_ assumptions)

Last updated: Dec 20 2023 at 11:08 UTC