mul_iSup

Mathlib.RingTheory.Ideal.Operations

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

English

I ⋅ (⨆ i, J_i) = ⨆ i, I ⋅ J_i.

Русский

I ⋅ (⨆ i, J_i) = ⨆ i, I ⋅ J_i.

LaTeX

$$$I \cdot \big(\bigsqcup_{i} J_i\big) = \bigsqcup_{i} (I \cdot J_i)$$$

Lean4

theorem mul_iSup {ι : Sort*} (J : ι → Ideal R) : I * (⨆ i, J i) = ⨆ i, I * J i :=
  Submodule.smul_iSup

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

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

Разделы

Аффилиация

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