Evaluating Polynomial Z on real number

Stream: new members

[Alex Gu]

How can I evaluate a polynomial with integer coefficients on a real number? I tried something like this, but it doesn't work. Also, not sure how to quickly find answers to these simple questions, any advice on more efficiently searching for things (rather than posting every time) would be helpful too!

theorem common_roots {P : Polynomial ℤ} :
  ∀ (x : ℝ), P.eval x = 0 → P.eval 0 = 0 := by sorry

[Aaron Liu]

Try using docs#Polynomial.map over docs#Int.castRingHom first before evaluating it.

[Aaron Liu]

As for searching things, I use loogle, moogle, leansearch, and the docs page.

[Alex Gu]

So like this?

theorem common_roots {P : Polynomial ℤ} :
  ∀ (x : ℝ), (P.map (Int.castRingHom ℝ)).eval x = 0 → (P.map (Int.castRingHom ℝ)).eval 0 = 0

[Aaron Liu]

P.eval 0 can also stay as-is

[Aaron Liu]

You can also use docs#Polynomial.eval₂

[Eric Wieser]

Or aeval