English
For polynomials p and q, eval₂ of p composed with q equals eval₂ of p with the inner evaluation applied to q.
Русский
Для многочленов p и q, eval₂ от p, применённого к q, равен eval₂ от p при внутри-вычислении q.
LaTeX
$$$\\mathrm{eval}_2 (\\text{algebraMap } R S) x \\bigl(p.\\mathrm{comp} q\\bigr) = \\mathrm{eval}_2 (\\text{algebraMap } R S) (\\mathrm{eval}_2 (\\text{algebraMap } R S) x q) p$$$
Lean4
@[simp]
theorem eval₂_comp' : eval₂ (algebraMap R S) x (p.comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) p := by
induction p using Polynomial.induction_on' with
| add r s hr hs => simp only [add_comp, eval₂_add, hr, hs]
| monomial n a => simp only [monomial_comp, eval₂_mul', eval₂_C, eval₂_monomial, eval₂_pow']
