instNSMul — Mathlib

English

There is a natural-number scalar multiplication on the restricted product, defined coordinatewise using the natural-number action on each fiber: (n · x)_i = n · x_i.

Русский

Существует умножение на натуральное число на ограниченном произведении, задаваемое по координатам: (n·x)_i = n·x_i.

LaTeX

$$$ (n \cdot x)_i = n \cdot x_i \quad (\forall i). $$$

Lean4

instance instNSMul [Π i, AddMonoid (R i)] [∀ i, AddSubmonoidClass (S i) (R i)] : SMul ℕ (Πʳ i, [R i, B i]_[𝓕]) where
  smul n x := ⟨fun i ↦ n • (x i), x.2.mono fun _ hi ↦ nsmul_mem hi n⟩

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