English
For a nontrivial R, for m ∈ M and S ⊆ M, the image of m lies in span of the images of S iff m ∈ S.
Русский
Пусть R ненулевой, тогда образ m принадлежит линейному замыканию образов S тогда и только тогда, когда m ∈ S.
LaTeX
$$$\\text{of}'_R M m \\in \\operatorname{span}_R\\bigl(\\mathrm{of}'_R M'' S\\bigr) \\iff m \\in S$$$
Lean4
/-- The image of an element `m : M` in `R[M]` belongs the submodule generated by
`S : Set M` if and only if `m ∈ S`. -/
theorem of'_mem_span [Nontrivial R] {m : M} {S : Set M} : of' R M m ∈ span R (of' R M '' S) ↔ m ∈ S :=
by
refine ⟨fun h => ?_, fun h => Submodule.subset_span <| Set.mem_image_of_mem (of R M) h⟩
unfold of' at h
rw [← Finsupp.supported_eq_span_single, Finsupp.mem_supported, Finsupp.support_single_ne_zero _ (one_ne_zero' R)] at h
simpa using h
