hasIntScalar — Mathlib

English

There is an integer-scalar action on DFinsupp when each β_i is an additive group, defined by (z • v)(i) = z • v(i).

Русский

Существует действие целочисленного скаляра на DFinsupp, если каждый β_i — аддитивная группа; задано как (z • v)(i) = z • v(i).

LaTeX

$$$ \text{hasIntScalar} \quad [\forall i, AddGroup (β i)] : SMul \mathbb{Z} (Π₀ i, β i) $$$

Lean4

/-- Note the general `SMul` instance doesn't apply as `ℤ` is not distributive
unless `β i`'s addition is commutative. -/
instance hasIntScalar [∀ i, AddGroup (β i)] : SMul ℤ (Π₀ i, β i) :=
  ⟨fun c v => v.mapRange (fun _ => (c • ·)) fun _ => zsmul_zero _⟩

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