coeSubmodule_span_singleton — Mathlib

English

For x ∈ R, the image of the principal ideal generated by x under coeSubmodule is the span of algebraMap(x): coeSubmodule_span_singleton x = span{ algebraMap_R_S x }.

Русский

Образ идеала, порожденного x, равен одиночной порождающей в S: coeSubmodule_span_singleton x = span{ algebraMap_R_S x }.

LaTeX

$$coeSubmodule_span_singleton : coeSubmodule S (Ideal.span { x }) = Submodule.span R {(algebraMap R S) x}$$

Lean4

theorem coeSubmodule_span_singleton (x : R) :
    coeSubmodule S (Ideal.span { x }) = Submodule.span R {(algebraMap R S) x} := by
  rw [coeSubmodule_span, Set.image_singleton]

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