smeval_C_mul — Mathlib

English

The smeval map is linear in constants: smeval(C(r)·p) = r·smeval(p).

Русский

Образовательная карта smeval линейна по константам: smeval(C(r)·p) = r·smeval(p).

LaTeX

$$$ (C\, r \cdot p).\,smeval\, x = r \cdot p.smeval\, x$$$

Lean4

theorem smeval_C_mul : (C r * p).smeval x = r • p.smeval x := by
  induction p using Polynomial.induction_on' with
  | add p q ph qh => simp only [mul_add, smeval_add, ph, qh, smul_add]
  | monomial n b => simp only [C_mul_monomial, smeval_monomial, mul_smul]

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