English
Let b be an S-basis of M. Under suitable hypotheses on the rings R ⊆ S (e.g., R is a commutative ring and Algebra R S has no zero-smul divisors), the R-span of the range of b has an R-basis, obtained by restricting scalars from S to R.
Русский
Пусть b — S-базис M. При подходящих условиях на кольца R и S (например, R — коммутативное кольцо, нет нулевых делителей в умножении), подпространство, порождаемое базисом b над R, имеет базис над R, полученный ограничением скаляров.
LaTeX
$$$\\text{restrictScalars} : Basis\\ ι\\ R\\ (\\mathrm{span}_R (\\mathrm{Set.range}\\, b))$$$
Lean4
/-- Let `b` be an `S`-basis of `M`. Let `R` be a CommRing such that `Algebra R S` has no zero smul
divisors, then the submodule of `M` spanned by `b` over `R` admits `b` as an `R`-basis. -/
noncomputable def restrictScalars : Basis ι R (span R (Set.range b)) :=
Basis.span (b.linearIndependent.restrict_scalars (smul_left_injective R one_ne_zero))
