English
If b is a basis for S over R and x ≠ 0, then the ith vector of the basis for span({x}) equals x times the ith basis vector, i.e., (basisSpanSingleton b hx)_i = x · b_i.
Русский
Если b — базис S над R и x ≠ 0, то i-й вектор базиса span({x}) равен x·b_i, т.е. (basisSpanSingleton b hx)_i = x·b_i.
LaTeX
$$$(\mathrm{basisSpanSingleton}\\, b\\, hx)_i = x \\cdot b_i$$$
Lean4
@[simp]
theorem basisSpanSingleton_apply (b : Basis ι R S) {x : S} (hx : x ≠ 0) (i : ι) :
(basisSpanSingleton b hx i : S) = x * b i := by
simp only [basisSpanSingleton, Basis.map_apply, LinearEquiv.trans_apply, Submodule.restrictScalarsEquiv_apply,
LinearEquiv.ofInjective_apply, LinearEquiv.coe_ofEq_apply, LinearEquiv.restrictScalars_apply,
LinearMap.mulLeft_apply]
