English
If the index set ι is finite and b is a basis of P, then x ∈ P iff there exists a function c : ι → R with x = ∑ i, c i • (b i).
Русский
Если множество индексов ι конечно и b является базисом P, то x принадлежит P тогда и только тогда, если существует функция c : ι → R такая, что x = ∑ i, c i • b_i.
LaTeX
$$$x \\in P \\iff \\exists c : ι \\to R,\\ x = \\sum_i c(i) \\cdot (b i : M)$$$
Lean4
/-- If the submodule `P` has a finite basis,
`x ∈ P` iff it is a linear combination of basis vectors. -/
theorem mem_submodule_iff' [Fintype ι] {P : Submodule R M} (b : Basis ι R P) {x : M} :
x ∈ P ↔ ∃ c : ι → R, x = ∑ i, c i • (b i : M) :=
b.mem_submodule_iff.trans <|
Finsupp.equivFunOnFinite.exists_congr_left.trans <|
exists_congr fun c => by simp [Finsupp.sum_fintype, Finsupp.equivFunOnFinite]
