eval_zero_map — Mathlib

English

For any f and polynomial p, the constant term of the mapped polynomial at 0 equals f applied to the constant term of p.

Русский

Для любого f и полинома p постоянный член отображённого полинома равен f применённому к постоянному члену p.

LaTeX

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

Lean4

@[simp]
theorem eval_zero_map (f : R →+* S) (p : R[X]) : (p.map f).eval 0 = f (p.eval 0) := by simp [← coeff_zero_eq_eval_zero]

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