English
For any f in MvPolynomial PUnit R, and φ: R →+* S, and a : PUnit → S, the equality holds: ((pUnitAlgEquiv R) f) evaluated by φ equals f evaluated by φ along a.
Русский
Для f ∈ MvPolynomial PUnit R, и отображений φ: R →+* S, a : PUnit → S, выполняется равенство: eval₂_(pUnitAlgEquiv R) f по φ равно eval₂ f по φ и a.
LaTeX
$$$$ ((pUnitAlgEquiv \\; R) f : \\text{Polynomial } R).eval₂ \\; φ \\; (a) = f.\\text{eval₂ } \\; φ \\; a. $$$$
Lean4
theorem eval₂_pUnitAlgEquiv {f : MvPolynomial PUnit R} {φ : R →+* S} {a : PUnit → S} :
((MvPolynomial.pUnitAlgEquiv R) f : Polynomial R).eval₂ φ (a default) = f.eval₂ φ a :=
by
simp only [MvPolynomial.pUnitAlgEquiv_apply]
induction f using MvPolynomial.induction_on' with
| monomial d r => simp
| add f g hf hg => simp [hf, hg]
