English
The image of m in MonoidAlgebra lies in the span of the image of S iff m ∈ S.
Русский
Образ м в MonoidAlgebra лежит в span образов S тогда и только тогда, когда m ∈ S.
LaTeX
$$$\\mathrm{of}_R M m \\in \\operatorname{span}_R(\\mathrm{of}_R M'' S) \\iff m \\in S$$$
Lean4
/-- The image of an element `m : M` in `MonoidAlgebra R M` belongs the submodule generated by
`S : Set M` if and only if `m ∈ S`. -/
theorem of_mem_span_of_iff [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⟩
dsimp [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
