instModuleOfSMulCommClass — Mathlib

English

The function space X →ₑ[σ] Y inherits a module structure over R, given that X and Y carry compatible actions and R is a ring acting compatibly.

Русский

Пространство функций X→ₑ[σ]Y имеет структуру модуля над R при условии совместимости действий.

LaTeX

$$$(X \to_{\sigma} Y)$ is a module over $R$ when $R$ acts compatibly on X and Y.$$

Lean4

instance [AddCommMonoid Y] [Semiring R] [SMul M X] [DistribSMul N Y] [Module R Y] [SMulCommClass N R Y] :
    Module R (X →ₑ[σ] Y) where
  add_smul _ _ _ := ext fun _ ↦ add_smul _ _ _
  zero_smul _ := ext fun _ ↦ zero_smul R _

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