English
A distributive multiplicative action of a monoid α on an additive monoid β yields a distributive multiplicative action on Set β; i.e., the action respects addition and zero on sets.
Русский
Распространённое по умножению действие моноида α на аддитивный моноид β порождает распределённое умножающее действие на Set β; т.е. действие сохраняет сумму и ноль на множествах.
LaTeX
$$$ [Monoid \ α] [AddMonoid \ β] [DistribMulAction \ α \ β] : DistribMulAction \ α (Set \ β) $$$
Lean4
/-- A distributive multiplicative action of a monoid on an additive monoid `β` gives a distributive
multiplicative action on `Set β`. -/
protected noncomputable def distribMulActionSet [Monoid α] [AddMonoid β] [DistribMulAction α β] :
DistribMulAction α (Set β) where
smul_add := smul_add
smul_zero := smul_zero
