span_image — Mathlib

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

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