instMulActionCarrierVFintypeCat

Mathlib.CategoryTheory.Action.Concrete

URI: https://scilib.ai/kg/mathlib#Action.instMulActionCarrierVFintypeCat

English

Definition giving a MulAction on the carrier of X in Action.FintypeCat.

Русский

Определение MulAction на носителе X в Action.FintypeCat.

LaTeX

$$$\text{MulActionCarrier}$$$

Lean4

instance {G : Type*} [Monoid G] (X : Action FintypeCat G) : MulAction G X.V :=
  Action.instMulAction X

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

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

Разделы

Аффилиация

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