constantCoeff_map — Mathlib

English

The constant term commutes with coefficient maps: applying map f to a polynomial and then taking its constant coefficient equals applying f to the constant coefficient of the polynomial.

Русский

Постоянный член полинома сохраняется при отображении коэффициентов: constantCoeff (map f φ) = f (constantCoeff φ).

LaTeX

$$$\\\\mathrm{constantCoeff}(\\\\mathrm{map}_f \\\\varphi) = f\\\\left(\\\\mathrm{constantCoeff}\\\\varphi\\\\right)$$$

Lean4

@[simp]
theorem constantCoeff_map (f : R →+* S₁) (φ : MvPolynomial σ R) :
    constantCoeff (MvPolynomial.map f φ) = f (constantCoeff φ) :=
  coeff_map f φ 0

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