instSMulCommClass — Mathlib

English

The direct sum ∑ i M_i inherits a commuting action of two scalar types R and S whenever each component M_i does, i.e., SMulCommClass R S (⨁ i, M_i).

Русский

Прямая сумма ∑ i M_i наследует коммутативное действие двух скаляров R и S, если соответствующие свойства выполняются на каждом компоненте M_i.

LaTeX

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

Lean4

instance {S : Type*} [Semiring S] [∀ i, Module S (M i)] [∀ i, SMulCommClass R S (M i)] : SMulCommClass R S (⨁ i, M i) :=
  DFinsupp.smulCommClass

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