sup_mul

Mathlib.Algebra.Algebra.Operations

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

English

Left distributivity: (M ⊔ N) * P = M * P ⊔ N * P.

Русский

Левая дистрибутивность: (M ⊔ N) * P = M * P ⊔ N * P.

LaTeX

$$$ (M \sqcup N) * P = M * P \sqcup N * P $$$

Lean4

theorem sup_mul : (M ⊔ N) * P = M * P ⊔ N * P :=
  sup_smul _ _ _

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

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

Разделы

Аффилиация

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