smul_def

Mathlib.Algebra.Module.Submodule.Pointwise

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

English

The smul of a submodule equals the span of its smul: a • S = span(a • S).

Русский

Смул подмодуля равен поряду: a • S = span(a • S).

LaTeX

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

Lean4

theorem smul_def (a : α) (S : Submodule R M) : a • S = span R (a • S : Set M) := by simp [← smul_span]

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

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

Разделы

Аффилиация

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