smul_closure

Mathlib.RingTheory.Ideal.Pointwise

URI: https://scilib.ai/kg/mathlib#Ideal.smul_closure

English

The image of span s under a is span of a•s; i.e., a•span(s) = span(a•s).

Русский

Образ пространства span(s) под действием a это span(a•s).

LaTeX

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

Lean4

theorem smul_closure (a : M) (s : Set R) : a • span s = span (a • s) :=
  Ideal.map_span _ _

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

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

Разделы

Аффилиация

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