ZSMul — Mathlib

English

There is a natural ℤ-action on Set α by repeated pointwise addition/subtraction.

Русский

Существует естественное действие целых чисел на Set α через поэлементное сложение и вычитание.

LaTeX

$$$$ z \cdot S = \begin{cases} S + \cdots + S & z>0 \\\\ {0} & z=0 \\\\ -S - \cdots - S & z<0 \end{cases}, \quad -S = \{ -x \mid x \in S \}. $$$$

Lean4

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

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