smul_sup

Mathlib.Algebra.Algebra.Operations

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

← MathLib Explorer

English

Multiplication distributes over join: I • (N ⊔ P) = (I • N) ⊔ (I • P).

Русский

Умножение распределяется по суммации: I • (N ⊔ P) = (I • N) ⊔ (I • P).

LaTeX

$$$ I \\cdot (N \\vee P) = I \\cdot N \\vee I \\cdot P $$$

Lean4

theorem smul_sup : I • (N ⊔ P) = I • N ⊔ I • P :=
  toAddSubmonoid_injective <| by simp only [smul_toAddSubmonoid, sup_toAddSubmonoid, AddSubmonoid.addSubmonoid_smul_sup]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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