module — Mathlib

English

The construction Endows k[G] with a module structure over R, via Finsupp module, turning AddMonoidAlgebra k G into an R-module when R and k are semirings and k is an R-module.

Русский

Конструкция превращает k[G] в модуль над R через Finsupp-модуль, когда R и k — полугруппы и k является модулем над R.

LaTeX

$$$$\text{Module } R\ k[G] = \text{Finsupp.module } G\ k.$$$$

Lean4

instance module [Semiring R] [Semiring k] [Module R k] : Module R k[G] :=
  Finsupp.module G k

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