iSup_mul

Mathlib.RingTheory.Ideal.Operations

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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