smeval_mul — Mathlib

English

Smeval preserves multiplication: smeval_x(p q) = smeval_x(p) · smeval_x(q).

Русский

Smeval сохраняет умножение: smeval_x(p q) = smeval_x(p) · smeval_x(q).

LaTeX

$$$ (p \cdot q).smeval\ x = p.smeval\ x \cdot q.smeval\ x $$$

Lean4

theorem smeval_mul : (p * q).smeval x = p.smeval x * q.smeval x := by
  induction p using Polynomial.induction_on' with
  | add r s hr hs => simp only [hr, hs, smeval_add, add_mul]
  | monomial n a => simp only [smeval_monomial, smeval_monomial_mul, smul_mul_assoc]

Похожие утверждения