English
Given a monoid α and a MulAction α on β, there is a natural MulAction of α on Filter β defined by smul, satisfying the usual action axioms.
Русский
Пусть α — моноид и есть действие α на β; тогда существует естественное действие α на Filter β, задаваемое smul и удовлетворяющее обычным аксиомам действия.
LaTeX
$$$\\mathrm{MulAction}\\; \\alpha\\; (\\mathrm{Filter}(\\beta)).$$$
Lean4
/-- A multiplicative action of a monoid on a type `β` gives a multiplicative action on `Filter β`.
-/
@[to_additive /-- An additive action of an additive monoid on a type `β` gives an additive action on
`Filter β`. -/
]
protected def mulActionFilter [Monoid α] [MulAction α β] : MulAction α (Filter β)
where
mul_smul a b f := by simp only [← Filter.map_smul, map_map, Function.comp_def, ← mul_smul]
one_smul f := by simp only [← Filter.map_smul, one_smul, map_id']
