module

Mathlib.Algebra.TrivSqZeroExt

URI: https://scilib.ai/kg/mathlib#TrivSqZeroExt.module

English

If S is a semiring, and R,M are additive monoids with module structures over S, then tsze R M is an S-module.

Русский

Если S — полугруппа по модулю, и R,M имеют структуры модуля над S, то tsze R M является S-модулем.

LaTeX

$$Module S (tsze R M)$$

Lean4

instance module [Semiring S] [AddCommMonoid R] [AddCommMonoid M] [Module S R] [Module S M] : Module S (tsze R M) :=
  Prod.instModule

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru