pointwiseModule — Mathlib

English

There is a module structure on Finsupp α β over the function space α → β, given by the pointwise scalar action.

Русский

На Finsupp α β над пространством функций α → β задана структура модуля посредством точечного скалярного действия.

LaTeX

$$$\\text{Module } (α \\to β) \\ (Finsupp \\ α β)$$$

Lean4

/-- The pointwise multiplicative action of functions on finitely supported functions -/
instance pointwiseModule [Semiring β] : Module (α → β) (α →₀ β) :=
  Function.Injective.module _ coeFnAddHom DFunLike.coe_injective coe_pointwise_smul

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