map_subtype_span_singleton — Mathlib

English

For p ⊆ M and x ∈ p, the image of span_R{x} under the subtype map p.subtype is the span of x inside M.

Русский

Пусть p — подмодуль M и x ∈ p. Образ порожденного множества {x} под включением p.subtype в M равен порожденному подмодулю в M, порожденному x.

LaTeX

$$$$ \\operatorname{map}_{p}(\\operatorname{span}_R(\\{x\\})) = \\operatorname{span}_R(\\{x\\}) $$$$

Lean4

@[simp]
theorem map_subtype_span_singleton {p : Submodule R M} (x : p) : map p.subtype (R ∙ x) = R ∙ (x : M) := by
  simp [← span_image]

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