eval_natCast_map — Mathlib

English

For any natural n, (p.map f).eval (n as in S) equals f(p.eval n).

Русский

Для любого натурального n, (p.map f).eval (n) равно f(p.eval n).

LaTeX

$$$ (p.map f).eval (n : S) = f (p.eval n) $$$

Lean4

@[simp]
theorem eval_natCast_map (f : R →+* S) (p : R[X]) (n : ℕ) : (p.map f).eval (n : S) = f (p.eval n) := 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_natCast f, eval_monomial, map_monomial, f.map_pow, f.map_mul]

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