mul_subset_mul

Mathlib.Algebra.Algebra.Operations

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

English

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

Русский

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

LaTeX

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

Lean4

theorem mul_subset_mul : (↑M : Set A) * (↑N : Set A) ⊆ (↑(M * N) : Set A) :=
  smul_subset_smul _ _

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

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

Разделы

Аффилиация

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