mulAction

Mathlib.Algebra.TrivSqZeroExt

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

English

If S acts on R and M, then S acts on tsze R M via the product action.

Русский

Если S действует на R и M, то S действует на tsze R M через произведенное действие.

LaTeX

$$MulAction S (tsze R M)$$

Lean4

instance mulAction [Monoid S] [MulAction S R] [MulAction S M] : MulAction S (tsze R M) :=
  Prod.mulAction

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

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

Разделы

Аффилиация

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