instModule — Mathlib

English

Let R be a semiring, E an additive group with an R-module structure, and A an arbitrary type. Then the type WithCStarModule A E is canonically an R-module, with the R-action coming from E (via the underlying identification).

Русский

Пусть R — полукольцо; E — добавочная группа с R-модульной структурой; A — произвольный тип. Тогда тип WithCStarModule A E естественным образом является R-модулем, причём действие скаляров берётся от E.

LaTeX

$$$ (WithCStarModule A E) \text{ is an } R\text{-module with } r \cdot x = (r \cdot_E) x$$$

Lean4

instance instModule {R : Type*} [Semiring R] [AddCommGroup E] [Module R E] : Module R C⋆ᵐᵒᵈ(A, E) :=
  ‹Module R E›

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