instModuleCoeOfSMulMemClass — Mathlib

English

If each fiber is a Module over a ring, then the restricted product carries a module structure with fiberwise scalar multiplication.

Русский

Если каждое волокно является модулем над кольцом, ограниченное произведение имеет модульную структуру с покоординатным скаляром.

LaTeX

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

Lean4

instance {R₀ : Type*} [Semiring R₀] [Π i, AddCommMonoid (R i)] [Π i, Module R₀ (R i)]
    [∀ i, AddSubmonoidClass (S i) (R i)] [∀ i, SMulMemClass (S i) R₀ (R i)] : Module R₀ (Πʳ i, [R i, B i]_[𝓕]) :=
  DFunLike.coe_injective.module R₀ (M := Π i, R i) coeAddMonoidHom (fun _ _ ↦ rfl)

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