English
There is a natural-power operation on Filter α defined by repeated pointwise multiplication: s^n is obtained by multiplying s with itself n times.
Русский
Существует естественное возведение фильтра в степень n: s^n получается путём повторного умножения на себя n раз.
LaTeX
$$$\forall s \in \mathrm{Filter}(\alpha),\ \forall n \in \mathbb{N},\ s^n = \underbrace{s * s * \cdots * s}_{n\text{ times}}.$$$
Lean4
/-- Repeated pointwise multiplication (not the same as pointwise repeated multiplication!) of a
`Filter`. See Note [pointwise nat action]. -/
@[to_additive existing]
protected def instNPow [One α] [Mul α] : Pow (Filter α) ℕ :=
⟨fun s n => npowRec n s⟩
