smul_sup'

Mathlib.Algebra.Module.Submodule.Pointwise

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

English

The smul action distributes over sup: a · (S ⊔ T) = a · S ⊔ a · T.

Русский

Действие смула распределяется над объединением: a · (S ⊔ T) = a · S ⊔ a · T.

LaTeX

$$$a \\cdot (S \\sqcup T) = (a \\cdot S) \\sqcup (a \\cdot T)$$$

Lean4

/-- See also `Submodule.smul_sup`. -/
theorem smul_sup' (a : α) (S T : Submodule R M) : a • (S ⊔ T) = a • S ⊔ a • T :=
  map_sup _ _ _

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

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

Разделы

Аффилиация

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