smul_sup

Mathlib.Algebra.Ring.Subring.Pointwise

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

English

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 : Subring R) : a • (S ⊔ T) = a • S ⊔ a • T :=
  map_sup _ _ _

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

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

Разделы

Аффилиация

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