English
For a finite subset s of M ⊗ N there exists a finitely generated submodule N' ⊆ N such that s ⊆ range (N' .subtype.lTensor M).
Русский
Для конечного подмножества s ⊂ M ⊗ N существует порожденное конечной величиной N' ⊆ N такое, что s ⊆ образ (N' .subtype.lTensor M).
LaTeX
$$$\exists N' \le N,\ Module.Finite R N',\ s \subseteq \mathrm{range}(N'.subtype.lTensor M)$$$
Lean4
/-- For any element `x` of `M ⊗[R] N`, there exists a finite subset `{ (m_i, n_i) }`
of `M × N`, such that `x` is equal to the sum of `m_i ⊗ₜ[R] n_i`. -/
theorem exists_finset (x : M ⊗[R] N) : ∃ S : Finset (M × N), x = S.sum fun i ↦ i.1 ⊗ₜ[R] i.2 :=
by
obtain ⟨S, h⟩ := exists_finsupp_left x
use S.graph
rw [h, Finsupp.sum]
apply Finset.sum_nbij' (fun m ↦ ⟨m, S m⟩) Prod.fst <;> simp
