eval₂_mul' — Mathlib

English

For polynomials p and q with coefficients in R, the evaluation under φ with a linear map preserves multiplication: (p·q) eval₂ = p eval₂ · q eval₂.

Русский

Для многочленов p и q с коэффициентами в R сохранение под eval₂ по линейному отображению сохраняет умножение: (p·q) eval₂ = (p eval₂) · (q eval₂).

LaTeX

$$$ (p \\cdot q).eval_2 (\\text{algebraMap } R S) x = p.\\ eval_2 (\\text{algebraMap } R S) x \\cdot q.\\ eval_2 (\\text{algebraMap } R S) x$$$

Lean4

@[simp]
theorem eval₂_mul' : (p * q).eval₂ (algebraMap R S) x = p.eval₂ (algebraMap R S) x * q.eval₂ (algebraMap R S) x := by
  exact eval₂_mul_noncomm _ _ fun k => Algebra.commute_algebraMap_left (coeff q k) x

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