eval₂_const_pUnitAlgEquiv — Mathlib

English

For a polynomial f in PUnit, the evaluation with φ and a yields the same result as evaluating f after applying the inverse pUnitAlgEquiv and then φ.

Русский

Для многочлена f в PUnit, вычисление через φ и a совпадает с вычислением после применения обратного pUnitAlgEquiv, а затем φ.

LaTeX

$$$$ ((pUnitAlgEquiv R) f : \\text{Polynomial } R).eval₂ φ a = f.\\text{eval₂ } φ a. $$$$

Lean4

theorem eval₂_const_pUnitAlgEquiv {f : MvPolynomial PUnit R} {φ : R →+* S} {a : S} :
    ((MvPolynomial.pUnitAlgEquiv R) f : Polynomial R).eval₂ φ a = f.eval₂ φ (fun _ ↦ a) := by rw [← eval₂_pUnitAlgEquiv]

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