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