English
There is a natural-number action of the additive monoid (ℕ, +) on the set of filters on α, given by repeated pointwise addition. Concretely, n sends a filter f to its nth additive iterate.
Русский
Существует действие натуральных чисел на множество фильтров над α, задаваемое повторяющимся поэлементным сложением; действием n является n-разовое сложение фильтра f.
LaTeX
$$$\forall f \in \mathrm{Filter}(\alpha),\ \forall n \in \mathbb{N},\ n \cdot f = \mathrm{nsmulRec}\, n\, f.$$$
Lean4
/-- Repeated pointwise addition (not the same as pointwise repeated addition!) of a `Filter`. See
Note [pointwise nat action]. -/
protected def instNSMul [Zero α] [Add α] : SMul ℕ (Filter α) :=
⟨nsmulRec⟩
