English
If x belongs to the span of a in S (over R), then its image under the base change algebraMap S T lies in the span of the image of a in T.
Русский
Если x принадлежит спану a в S (над R), то его образ под отображением алгебраMap S T принадлежит спану образа a в T.
LaTeX
$$$\\\\text{If } x \\\\in \\\\operatorname{span}_R a, \\\\text{ then } \\\\mathrm{algebraMap} S T x \\\\in \\\\operatorname{span}_R\\\\left(\\\\mathrm{algebraMap} S T \\\\text{''} a\\\\right).$$
Lean4
theorem map_mem_span_algebraMap_image {S T : Type*} [CommSemiring S] [Semiring T] [Algebra R S] [Algebra R T]
[Algebra S T] [IsScalarTower R S T] (x : S) (a : Set S) (hx : x ∈ Submodule.span R a) :
algebraMap S T x ∈ Submodule.span R (algebraMap S T '' a) :=
by
rw [span_algebraMap_image_of_tower, mem_map]
exact ⟨x, hx, rfl⟩
