instZSMul — Mathlib

English

There is an action of the integers on Filter α by pointwise addition/subtraction, given by zsmulRec.

Русский

Существует действие целых чисел на Filter α путём поэлементного сложения и вычитания, заданное через zsmulRec.

LaTeX

$$$\forall f \in \mathrm{Filter}(\alpha),\ \forall n \in \mathbb{Z},\ n \cdot f = \mathrm{zsmulRec}\, n\, f.$$$

Lean4

/-- Repeated pointwise addition/subtraction (not the same as pointwise repeated
addition/subtraction!) of a `Filter`. See Note [pointwise nat action]. -/
protected def instZSMul [Zero α] [Add α] [Neg α] : SMul ℤ (Filter α) :=
  ⟨zsmulRec⟩

Похожие утверждения