iSup_mul

Mathlib.Algebra.Algebra.Operations

URI: https://scilib.ai/kg/mathlib#Submodule.iSup_mul

English

iSup version: (iSup t_i) • N = iSup (t_i • N).

Русский

Версия для iSup: (iSup t_i) • N = iSup (t_i • N).

LaTeX

$$$ (\bigvee_i t_i) \cdot N = \bigvee_i (t_i \cdot N) $$$

Lean4

theorem iSup_mul (s : ι → Submodule R A) (t : Submodule R A) : (⨆ i, s i) * t = ⨆ i, s i * t :=
  iSup_smul

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru