toDistribSMul — Mathlib

English

Let M be a monoid acting on an additive monoid A by a distributive action. Then this action induces a natural distributive scalar multiplication by M on A, i.e. A carries a DistribSMul M A structure.

Русский

Пусть M — моноид, действующий на аддитивный моноид A через дистрибутивное действие. Тогда это действие порождает естественное распределительное скалярное умножение M на A, то есть A получает структуру DistribSMul M A.

LaTeX

$$$\text{DistribMulAction}(M,A) \Rightarrow \text{DistribSMul}(M,A)$$$

Lean4

instance (priority := 100) toDistribSMul : DistribSMul M A :=
  { ‹DistribMulAction M A› with }

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