English
A distributive multiplicative action of a monoid α on an additive monoid β induces a distributive action on Filter β, i.e., smul distributes over addition in the filter context.
Русский
Расширение распределенного умножающего действия моноида α на аддитивный моноид β до Filter β сохраняет распределенность: умножение действует дистрибутивно над сложением внутри фильтров.
LaTeX
$$$\\mathrm{DistribMulAction}(\\alpha, \\mathrm{Filter}(\\beta)).$$$
Lean4
/-- A distributive multiplicative action of a monoid on an additive monoid `β` gives a distributive
multiplicative action on `Filter β`. -/
protected def distribMulActionFilter [Monoid α] [AddMonoid β] [DistribMulAction α β] : DistribMulAction α (Filter β)
where
smul_add _ _ _ := map_map₂_distrib <| smul_add _
smul_zero _ := (map_pure _ _).trans <| by rw [smul_zero, pure_zero]
