span_singleton_mul

Mathlib.Algebra.Algebra.Operations

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

English

Span {x} · P equals x times P, i.e., span {x} · P = x • P.

Русский

Объем {x} умножает подмодуль P: span{x} · P = x • P.

LaTeX

$$$\\operatorname{span} R \\{x\\} \\cdot P = x \\cdot P$$$

Lean4

theorem span_singleton_mul {x : A} {p : Submodule R A} : Submodule.span R { x } * p = x • p :=
  ext fun _ ↦ mem_span_singleton_mul

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

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

Разделы

Аффилиация

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