smul_sup

Mathlib.Algebra.Ring.Subsemiring.Pointwise

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

English

Smul distributes over join: a • (S ⊔ T) = (a • S) ⊔ (a • T).

Русский

Умножение по точечному действию распределяется по объединению: a • (S ⊔ T) = (a • S) ⊔ (a • T).

LaTeX

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

Lean4

theorem smul_sup (a : M) (S T : Subsemiring R) : a • (S ⊔ T) = a • S ⊔ a • T :=
  map_sup _ _ _

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

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

Разделы

Аффилиация

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