module — Mathlib

English

If R is a semiring and M an R-module, then the finsupp space α →₀ M inherits an R-module structure via the distributive action.

Русский

Если R — полукольцо, а M — модуль над R, то пространство Finsupp α M наследует структуру модуля над R через распределённое действие.

LaTeX

$$$[Semiring R][Module R M]\\Rightarrow Module R (\\alpha \\to_0 M)$$$

Lean4

instance module [Semiring R] [AddCommMonoid M] [Module R M] : Module R (α →₀ M) :=
  { toDistribMulAction := Finsupp.distribMulAction α M
    zero_smul := fun _ => ext fun _ => zero_smul _ _
    add_smul := fun _ _ _ => ext fun _ => add_smul _ _ _ }

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