coe_span_eq_span_of_surjective — Mathlib

English

If the algebra map from R to A is surjective, then the image of the span over R equals the span over R of the same generator set; i.e., the span is preserved under restriction of scalars.

Русский

Если алгебраическая карта R → A сюръективна, тогда образ линейной оболочки порождается над R совпадает при ограничении скаляров.

LaTeX

$$$$\\text{surjective} \\Rightarrow (\\operatorname{Submodule.cast}\\ldots)$$$$

Lean4

theorem coe_span_eq_span_of_surjective (h : Function.Surjective (algebraMap R A)) (s : Set M) :
    (Submodule.span A s : Set M) = Submodule.span R s :=
  congr_arg ((↑) : Submodule R M → Set M) (Submodule.restrictScalars_span R A h s)

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