English
For p ∈ R[X], x ∈ S, and m, n ∈ ℕ, the product p.smeval x times x^m times x^n is associative: p.smeval x · x^m · x^n = p.smeval x · (x^m · x^n).
Русский
Для p ∈ R[X], x ∈ S и m,n ∈ ℕ, произведение p.smeval x на x^m и затем на x^n ассоциативно: p.smeval x · x^m · x^n = p.smeval x · (x^m · x^n).
LaTeX
$$$$ p.smeval x \cdot x^m \cdot x^n = p.smeval x \cdot (x^m \cdot x^n). $$$$
Lean4
theorem smeval_at_zero : p.smeval (0 : S) = (p.coeff 0) • (1 : S) := by
induction p using Polynomial.induction_on' with
| add p q ph qh => simp_all only [smeval_add, coeff_add, add_smul]
| monomial n a =>
cases n with
| zero => simp only [monomial_zero_left, smeval_C, npow_zero, coeff_C_zero]
| succ n => rw [coeff_monomial_succ, smeval_monomial, npow_add, npow_one, mul_zero, zero_smul, smul_zero]
