span_image' — Mathlib

English

For a RingSurjective σ₁₂ and a semilinear map f, the span over R₂ of the image f''s equals the image of the span under f: span_{R₂}(f''s) = map f(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

@[simp] -- Should be replaced with `Submodule.span_image` when https://github.com/leanprover/lean4/pull/3701 is fixed.

theorem span_image' [RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) : span R₂ (f '' s) = map f (span R s) :=
  span_image _

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