English
Let a be a subset of R. Then the R-span of the image of a under the algebra map to S equals the image of the span of a under the corresponding linear map.
Русский
Пусть a ⊆ R. Тогда спан по R образа a через отображение алгебры R → S равен образу спана a под соответствующим линейным отображением.
LaTeX
$$$\\\\operatorname{span}_R\\\\left(\\\\mathrm{algebraMap} R S \\\\text{''} \\\\! a\\\\right) \\\\,=\\\\, \\\\left(\\\\operatorname{span}_R a\\\\right)\\\\.map \\\\left(\\\\mathrm{Algebra.linearMap} R S\\\\)$.$$
Lean4
/-- A variant of `Submodule.span_image` for `algebraMap`. -/
theorem span_algebraMap_image (a : Set R) :
Submodule.span R (algebraMap R S '' a) = (Submodule.span R a).map (Algebra.linearMap R S) :=
(Submodule.span_image <| Algebra.linearMap R S).trans rfl
