smul_sup

Mathlib.Algebra.Group.Subgroup.Pointwise

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

English

Scalar action distributes over the join (supremum) of two subgroups: 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

theorem smul_sup (a : α) (S T : Subgroup G) : a • (S ⊔ T) = a • S ⊔ a • T :=
  map_sup _ _ _

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

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

Разделы

Аффилиация

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