English
A multiplicative action of a monoid α on a monoid β induces a multiplicative action on the set β, i.e., α acts on the collection of subsets of β by image maps, respecting multiplication and identity.
Русский
Действие моноида α на моноид β порождает действие над множествами β: α действует на наборы подмножеств β через образ, сохраняя умножение и тождество.
LaTeX
$$$\\mathrm{MulDistribMulAction}(\\alpha,\\mathrm{Set}(\\beta)).$$$
Lean4
/-- A multiplicative action of a monoid on a monoid `β` gives a multiplicative action on `Set β`. -/
protected noncomputable def mulDistribMulActionFilter [Monoid α] [Monoid β] [MulDistribMulAction α β] :
MulDistribMulAction α (Set β)
where
smul_mul _ _ _ := image_image2_distrib <| smul_mul' _
smul_one _ := image_singleton.trans <| by rw [smul_one, singleton_one]
