instDistribMulAction'

Mathlib.Algebra.Order.GroupWithZero.Action.Synonym

URI: https://scilib.ai/kg/mathlib#Lex.instDistribMulAction'

English

The Lex construction carries a distributive action by G₀ on M₀.

Русский

Конструкция Lex содержит дисрибутивное действие G₀ на M₀.

LaTeX

$$$\text{DistribMulAction}(G_{0}, \mathrm{Lex}\,M_{0})$$$

Lean4

instance instDistribMulAction' [Monoid G₀] [AddMonoid M₀] [DistribMulAction G₀ M₀] : DistribMulAction G₀ (Lex M₀) :=
  ‹DistribMulAction G₀ M₀›

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

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

Разделы

Аффилиация

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