smulFinset — Mathlib

English

The action of a scalar on a Finset is defined by applying the scalar to every element: a • s = image (x ↦ a • x) s.

Русский

Действие скаляра на финсет определяется применением скаляра к каждому элементу: a • s = image (x ↦ a • x) s.

LaTeX

$$$a \cdot s = \operatorname{image}(x \mapsto a \cdot x)\, s$$$

Lean4

/-- The scaling of a finset `s` by a scalar `a`: `a • s = {a • x | x ∈ s}`. -/
@[to_additive /-- The translation of a finset `s` by a vector `a`: `a +ᵥ s = {a +ᵥ x | x ∈ s}`. -/
    ]
protected def smulFinset : SMul α (Finset β) where smul a := image <| (a • ·)

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