of_smul_of — Mathlib

English

The direct sum of graded components forms a module with the induced action from the graded ring.

Русский

Прямая сумма градационных компонент образует модуль с индуцированным действием из градаированного кольца.

LaTeX

$$$$ \\text{DirectSum.Gmodule module structure on } \\bigoplus_i M_i. $$$$

Lean4

theorem of_smul_of [DecidableEq ιA] [DecidableEq ιB] [GMonoid A] [Gmodule A M] {i j} (x : A i) (y : M j) :
    DirectSum.of A i x • of M j y = of M (i +ᵥ j) (GSMul.smul x y) := by simp

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