coeSubmodule_span — Mathlib

English

For a set s ⊆ R, the image under the algebra map spans in S correspond to the span of the image: coeSubmodule_span(s) = Submodule.span_R(algebraMap_R_S '' s).

Русский

Образ множества s под алгебраическим отображением порождает такой же функциональный образы в S: coeSubmodule_span(s) = Submodule.span_R(algebraMap_R_S '' s).

LaTeX

$$coeSubmodule_span : coeSubmodule S (Ideal.span s) = Submodule.span R (algebraMap R S '' s)$$

Lean4

@[simp]
theorem coeSubmodule_span (s : Set R) : coeSubmodule S (Ideal.span s) = Submodule.span R (algebraMap R S '' s) :=
  by
  rw [IsLocalization.coeSubmodule, Ideal.span, Submodule.map_span]
  rfl

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