English
There is an integer power operation on Filter α defined by zpowRec npowRec, giving s^n for integer n with possibly negative exponent.
Русский
Существует целочисленная степень фильтра: s^n определяется как zpowRec npowRec, позволяя отрицательные степени.
LaTeX
$$$\forall s \in \mathrm{Filter}(\alpha),\ \forall n \in \mathbb{Z},\ s^{n} = \mathrm{zpowRec}(\mathrm{npowRec}, n, s).$$$
Lean4
/-- Repeated pointwise multiplication/division (not the same as pointwise repeated
multiplication/division!) of a `Filter`. See Note [pointwise nat action]. -/
@[to_additive existing]
protected def instZPow [One α] [Mul α] [Inv α] : Pow (Filter α) ℤ :=
⟨fun s n => zpowRec npowRec n s⟩
