English
For x ∈ M, with SMulCommClass R R N, x ∈ sR • N iff there exists c: R →₀ N with finite support in sR and x = sum over r of c(r) with r • m.
Русский
Для x ∈ M верно: x ∈ sR • N тогда и только тогда, когда существует конечная сумма c: R →₀ N такая, что supp(c) ⊆ sR и x = ∑ (r) c(r) · (r • m).
LaTeX
$$$ x \in s_R \cdot N \ \iff\ \exists c: R \to_{0} N,\ (c.supp) \subseteq s_R \ \land\ x = c.sum (\lambda r m, r \cdot m) $$$
Lean4
theorem mem_set_smul (x : M) [SMulCommClass R R N] :
x ∈ sR • N ↔ ∃ (c : R →₀ N), (c.support : Set R) ⊆ sR ∧ x = c.sum fun r m ↦ r • m :=
by
fconstructor
· intro h
rw [set_smul_eq_map] at h
obtain ⟨c, hc, rfl⟩ := h
exact ⟨c, hc, rfl⟩
· rw [mem_set_smul_def, Submodule.mem_sInf]
rintro ⟨c, hc1, rfl⟩ p hp
rw [Finsupp.sum, AddSubmonoid.coe_finset_sum]
exact Submodule.sum_mem _ fun r hr ↦ hp (hc1 hr) (c _).2
