English
If σ₂,₂ surjects onto R₂ and f is a semilinear/linear map, then the span of the image f[s] over R₂ equals the image under f of the span of s over R: span_{R₂}(f''s) = map_f(span_R s).
Русский
Если отображение σ₁₂ действует сюрьективно и f — полилинейное отображение, то спан образа f(s) над R₂ равен образу пространства span_R(s) под f: span_{R₂}(f''s) = map_f(span_R s).
LaTeX
$$$$ \\operatorname{span}_{R_2}(f''s) = \\operatorname{map} f(\\operatorname{span}_R s). $$$$
Lean4
theorem span_image [RingHomSurjective σ₁₂] (f : F) : span R₂ (f '' s) = map f (span R s) :=
(map_span f s).symm