English
A multiplicative action of a monoid α on a type β induces a multiplicative action of Filter α on Filter β; the axioms follow from the corresponding ones for α and β through the smul defined on filters.
Русский
Умножающееся действие моноидa α на тип β порождает умножающееся действие Filter α на Filter β; аксиомы получаются из соответствующих аксиом для α и β через определение действия на фильтрах.
LaTeX
$$$\\mathrm{MulAction}(\\mathrm{Filter}(\\alpha), \\mathrm{Filter}(\\beta)).$$$
Lean4
/-- A multiplicative action of a monoid `α` on a type `β` gives a multiplicative action of
`Filter α` on `Filter β`. -/
@[to_additive /-- An additive action of an additive monoid `α` on a type `β` gives an additive
action of `Filter α` on `Filter β`. -/
]
protected def mulAction [Monoid α] [MulAction α β] : MulAction (Filter α) (Filter β)
where
one_smul f := map₂_pure_left.trans <| by simp_rw [one_smul, map_id']
mul_smul _ _ _ := map₂_assoc mul_smul
