English
The action of aeval on the polynomial equivPolynomial f equals the evaluation of the induced map: aeval x (equivPolynomial f) = eval x (map R (Algebra.linearMap S R) f).
Русский
Действие aeval на эквивалентность полиномов equivalPolynomial f совпадает с оценкой через отображение: aeval x (equivPolynomial f) = eval x (map R (Algebra.linearMap S R) f).
LaTeX
$$$\\mathrm{aeval}\\, x\\; (\\mathrm{equivPolynomial}\, f) = \\operatorname{eval} x (\\operatorname{map} R (\\mathrm{Algebra.linearMap} S R) f)$$$
Lean4
@[simp]
theorem aeval_equivPolynomial {S : Type*} [CommRing S] [Algebra S R] (f : PolynomialModule S S) (x : R) :
aeval x (equivPolynomial f) = eval x (map R (Algebra.linearMap S R) f) := by
induction f using induction_linear with
| zero => simp
| add f g e₁ e₂ => simp_rw [map_add, e₁, e₂]
| single i m =>
rw [equivPolynomial_single, aeval_monomial, mul_comm, map_single, Algebra.linearMap_apply, eval_single, smul_eq_mul]
