English
Let b be a Basis ι over R of S, and x ≠ 0 in S. Then there exists a Basis for span({x}) on S given by x·b_i.
Русский
Пусть b — базис модуля S над R; для x ≠ 0 существует базис для span({x}) на S, получаемый как x·b_i.
LaTeX
$$∃ b' : Basis ι R (span({x})) с b'_i = x · b_i$$
Lean4
/-- A basis on `S` gives a basis on `Ideal.span {x}`, by multiplying everything by `x`. -/
noncomputable def basisSpanSingleton (b : Basis ι R S) {x : S} (hx : x ≠ 0) : Basis ι R (span ({ x } : Set S)) :=
b.map <|
LinearEquiv.ofInjective (LinearMap.mulLeft R x) (mul_right_injective₀ hx) ≪≫ₗ
LinearEquiv.ofEq _ _
(by
ext
simp [mem_span_singleton', mul_comm]) ≪≫ₗ
(Submodule.restrictScalarsEquiv R S S (Ideal.span ({ x } : Set S))).restrictScalars R