instIsCentralScalar — Mathlib

English

If each M_i has a central R-scalar action, then the direct sum ⨁ i M_i also has a central R-scalar action: IsCentralScalar R (⨁ i, M_i).

Русский

Если на каждом компоненте M_i скалярное действие от R является центральным, то и на прямой сумме действует центральный R-скаляр.

LaTeX

$$$\\mathrm{IsCentralScalar}\\; R\\; (\\bigoplus_{i} M_i).$$$

Lean4

instance [∀ i, Module Rᵐᵒᵖ (M i)] [∀ i, IsCentralScalar R (M i)] : IsCentralScalar R (⨁ i, M i) :=
  DFinsupp.isCentralScalar

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