evalEval_smul — Mathlib

English

Evaluation commutes with scalar multiplication: (s • p).evalEval x y = s • p.evalEval x y.

Русский

Оценка коммутирует умножение на скаляр: (s • p).evalEval x y = s • p.evalEval x y.

LaTeX

$$$ (s \\cdot p).evalEval\\ x\\ y = s \\cdot p.evalEval\\ x\\ y $$$

Lean4

@[simp]
theorem evalEval_smul [DistribSMul S R] [IsScalarTower S R R] (x y : R) (s : S) (p : R[X][Y]) :
    (s • p).evalEval x y = s • p.evalEval x y := by simp only [evalEval, eval_smul]

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