mul_iSup

Mathlib.Algebra.Algebra.Operations

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

English

iSup version (alternate): (iSup s_i) * t = iSup (s_i * t).

Русский

Альтернативная версия iSup: (iSup s_i) * t = iSup (s_i * t).

LaTeX

$$$ (\bigvee_i s_i) * t = \bigvee_i (s_i * t) $$$

Lean4

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

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

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

Разделы

Аффилиация

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