English
Let i be a ring homomorphism R → S and x be an invertible element of S. For any polynomial f over R, the evaluation of reverse(f) at ⅟x, multiplied by x raised to the degree of f, equals the evaluation of f at x via i. In symbols: eval₂ i (⅟x) (reverse f) · x^{natDegree f} = eval₂ i x f.
Русский
Пусть i — кольцеобразное отображение R → S и пусть x является обратимым элементом S. Для любого многочлена f над R верно: eval₂ i (⅟x) (reverse f) · x^{natDegree f} = eval₂ i x f.
LaTeX
$$$$\\operatorname{eval}_2 i \\left( x^{-1} \\right) \\big( \\operatorname{reverse} f \\big) \\cdot x^{\\operatorname{natDegree} f} = \\operatorname{eval}_2 i x f.$$$$
Lean4
theorem eval₂_reverse_mul_pow (i : R →+* S) (x : S) [Invertible x] (f : R[X]) :
eval₂ i (⅟x) (reverse f) * x ^ f.natDegree = eval₂ i x f :=
eval₂_reflect_mul_pow i _ _ f le_rfl
