span_singleton_eq_range

Mathlib.LinearAlgebra.Span.Defs

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

English

For y ∈ M, the carrier of R ∙ y equals the range of the map r ↦ r • y.

Русский

Для y ∈ M носитель R ∙ y равен образу отображения r ↦ r • y.

LaTeX

$$$$ \\uparrow(R \\cdot y) = \\operatorname{range}( (\\cdot \\cdot y) : R \\to M ). $$$$

Lean4

theorem span_singleton_eq_range (y : M) : ↑(R ∙ y) = range ((· • y) : R → M) :=
  Set.ext fun _ => mem_span_singleton

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

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

Разделы

Аффилиация

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