instZSMul — Mathlib

English

If each fiber has an additive group structure, then the restricted product supports a Z-action (scalar multiplication by integers) coordinatewise: (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 instZSMul [Π i, SubNegMonoid (R i)] [∀ i, AddSubgroupClass (S i) (R i)] : SMul ℤ (Πʳ i, [R i, B i]_[𝓕]) where
  smul n x := ⟨fun i ↦ n • x i, x.2.mono fun _ hi ↦ zsmul_mem hi n⟩

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