hasNatScalar — Mathlib

English

There is a natural-number scalar action on the dependent function finitely supported type: (c, v) ↦ v.mapRange(λ _, c • _) with nsmul_zero as the zero map.

Русский

Существует действие натурального скаляра на DFinsupp: (c, v) ↦ v.mapRange(λ _, c • _).

LaTeX

$$$\text{SMul} \; \mathbb{N} \; (\Pi_{i} \beta i)$$$

Lean4

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

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