English
If a submodule P has a basis b, then an element x lies in P exactly when x can be expressed as a finite linear combination of the basis vectors b i with coefficients in the ambient ring. Equivalently, x ∈ P iff ∃ c : ι →₀ R such that x = ∑ i, c i • (b i : M).
Русский
Если подпространство P имеет базис b, то элемент x принадлежит P тогда и только тогда, когда x может быть выражен как конечное линейное сочетание базисных векторов b_i с коэффициентами из окружения. То есть x ∈ P тогда и только тогда, существует c : ι →₀ R такое, что x = ∑ i, c i • (b i).
LaTeX
$$$x \\in P \\iff \\exists c : ι \\to_0 R,\\ x = \\sum_i c(i) \\cdot (b i : M)$$$
Lean4
/-- If the submodule `P` has a basis, `x ∈ P` iff it is a linear combination of basis vectors. -/
theorem mem_submodule_iff {P : Submodule R M} (b : Basis ι R P) {x : M} :
x ∈ P ↔ ∃ c : ι →₀ R, x = Finsupp.sum c fun i x => x • (b i : M) :=
by
conv_lhs =>
rw [← P.range_subtype, ← Submodule.map_top, ← b.span_eq, Submodule.map_span, ← Set.range_comp, ←
Finsupp.range_linearCombination]
simp [@eq_comm _ x, Function.comp, Finsupp.linearCombination_apply]
