Evaluating bivariate polynomial at X

Stream: Is there code for X?

[Ahmad Alkhalawi]

Let p : R[X][Y]. Then I can't figure out how to substitute the X variable for something? I know you can do p.sum (fun i a => (aeval x a)*(X:K[X])^i) but is there a built-in way?

[Christian Merten]

I can only guess your precise setup, but you are probably looking for docs#Polynomial.map. You can then write

import Mathlib
variable {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
open Polynomial

noncomputable example (p : R[X][Y]) (x : S) : S[X] :=
  map (aeval x).toRingHom p

[Ahmad Alkhalawi]

That seems to work, thanks

[David Ang]

@Ahmad Alkhalawi maybe something in https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Polynomial/Bivariate.html might help?

[Ahmad Alkhalawi]

David Ang said:

Ahmad Alkhalawi maybe something in https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Polynomial/Bivariate.html might help?

I checked that already and couldn't find anything