hasSMulPi' — Mathlib

English

A variant of the above action: there is a SMul action of R[X] on S → T defined by (p • f)(x) = aeval x p · f x.

Русский

Вариант выше: существует действие R[X] на S → T, задаваемое (p • f)(x) = aeval x p · f x.

LaTeX

$$$$\text{HasSMulPi'}:\; SMul\; R[X]\; (S \to T), \; (p,f) \mapsto (x \mapsto (\operatorname{aeval}(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. -/
noncomputable def hasSMulPi' [CommSemiring R] [Semiring S] [Algebra R S] [SMul S T] : SMul R[X] (S → T) :=
  ⟨fun p f x => aeval x p • f x⟩

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