eval_intCast_map — Mathlib

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]

Похожие утверждения