eval_one_map — Mathlib

English

For any f and polynomial p, the evaluation at 1 commutes with mapping: (p.map f).eval 1 = f (p.eval 1).

Русский

Для любого f и полинома p вычисление при 1 коммутирует отображение: (p.map f).eval 1 = f (p.eval 1).

LaTeX

$$$ (p.map f).eval 1 = f (p.eval 1) $$$

Lean4

@[simp]
theorem eval_one_map (f : R →+* S) (p : R[X]) : (p.map f).eval 1 = f (p.eval 1) := 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 [one_pow, mul_one, eval_monomial, map_monomial]

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