English
Let A be a ring and rel a family of relations indexed by G. The A-submodule generated by all the images of the relation generators under the relation map equals the image (range) of the relation map. Equivalently, the range of the map equals the span of the relation generators.
Русский
Пусть A — кольцо и задана family отношений, индексируемая множество G. Подмодуль над A, порождённый всеми образами генераторов отношений под отображением отношений, совпадает с образами отображения отношений (range). Иными словами, образ отображения совпадает с оболочкой отношений.
LaTeX
$$$\operatorname{range}(\text{relations.map}) = \operatorname{span}_A\bigl(\mathrm{Set.range}(\text{relations.relation})\bigr)$$$
Lean4
@[simp]
theorem range_map : LinearMap.range relations.map = Submodule.span A (Set.range relations.relation) :=
Finsupp.range_linearCombination _
