mul_sup

Mathlib.Algebra.Algebra.Operations

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

English

Repeated: MulLeftMono for Submodule

Русский

Повторение: MulLeftMono для Submodule

LaTeX

$$$\text{Multiplication on the left is monotone: }$$$

Lean4

theorem mul_sup : M * (N ⊔ P) = M * N ⊔ M * P :=
  smul_sup _ _ _

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

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

Разделы

Аффилиация

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