English
For rings R,S and integer i, (p.map f).eval i = f(p.eval i).
Русский
Для колец R,S и целого i, (p.map f).eval i = f(p.eval i).
LaTeX
$$$ (p.map f).eval (i) = f (p.eval i) $$$
Lean4
@[simp]
theorem eval_intCast_map {R S : Type*} [Ring R] [Ring S] (f : R →+* S) (p : R[X]) (i : ℤ) :
(p.map f).eval (i : S) = f (p.eval i) := by
induction p using Polynomial.induction_on' with
| add p q hp hq => simp only [hp, hq, Polynomial.map_add, RingHom.map_add, eval_add]
| monomial n r => simp only [map_intCast, eval_monomial, map_monomial, map_pow, map_mul]