zsmul — Mathlib

English

There is an integer-scalar action on Finset α, defined as repeated pointwise addition/subtraction.

Русский

Существует целочисленное действие на Finset α, задаваемое повторяющимся поэлементным сложением/вычитанием.

LaTeX

$$$$ \\text{Finset }\\alpha \\text{ carries an }\\mathbb{Z}\\text{-action by pointwise addition/subtraction} $$$$

Lean4

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

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