English
If I has a finite basis b over R, then x ∈ I iff x is a finite R-linear combination of the basis elements.
Русский
Если I имеет конечный базис b над R, то x ∈ I тогда и только тогда, когда x выражается как конечное линейное сочетание по R базисных элементов.
LaTeX
$$x ∈ I ⇔ ∃ c: ι → R, x = ∑ i, c i · b i$$
Lean4
/-- If `I : Ideal S` has a finite basis over `R`,
`x ∈ I` iff it is a linear combination of basis vectors. -/
theorem mem_ideal_iff' {ι R S : Type*} [Fintype ι] [CommSemiring R] [Semiring S] [Algebra R S] {I : Ideal S}
(b : Basis ι R I) {x : S} : x ∈ I ↔ ∃ c : ι → R, x = ∑ i, c i • (b i : S) :=
(b.map ((I.restrictScalarsEquiv R _ _).restrictScalars R).symm).mem_submodule_iff'
