hasSMulPi — Mathlib

English

There is a scalar action of polynomials with coefficients in R on the set of functions from R to S, given by (p • f)(x) = eval x p · f x.

Русский

Существует действие полиномов над функциями из R в S, заданное формулой (p • f)(x) = eval(x, p) · f(x).

LaTeX

$$$$\text{SMul } \_ : R[X] \times (R \to S) \to (R \to S), \; (p,f) \mapsto (x \mapsto \operatorname{eval}(x,p) \cdot f(x)). $$$$

Lean4

/-- This is not an instance as it forms a diamond with `Pi.instSMul`.

See the `instance_diamonds` test for details. -/
def hasSMulPi [Semiring R] [SMul R S] : SMul R[X] (R → S) :=
  ⟨fun p f x => eval x p • f x⟩

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