smul_span

Mathlib.Algebra.Module.Submodule.Pointwise

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

English

The smul of a span equals the span of the smul of the generating set: a • span s = span (a • s).

Русский

Смул-образ рост spans: a • span(s) = span(a • s).

LaTeX

$$$a \\cdot \\mathrm{span}(s) = \\mathrm{span}(a \\cdot s)$$$

Lean4

theorem smul_span (a : α) (s : Set M) : a • span R s = span R (a • s) :=
  map_span _ _

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

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

Разделы

Аффилиация

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