English
If a family v is linearly independent over R, and a linear map f acts compatibly with the scalar action, then restricting scalars from R to R and composing with f preserves linear independence, provided certain injectivity conditions hold on the coefficients.
Русский
Если семейство в линейно независимо над R, и линейное отображение f согласовано с скалярами, то переход на другой основание скаляров и композиция с f сохраняют линейную независимость при необходимых условиях инъективности коэффициентов.
LaTeX
$$$\text{LinearIndependent}_R(v) \Rightarrow \text{LinearIndependent}_{R'}(f \circ v)$$$
Lean4
theorem restrict_scalars' [Semiring K] [SMulWithZero R K] [Module K M] [IsScalarTower R K M] [FaithfulSMul R K]
[IsScalarTower R K K] {v : ι → M} (li : LinearIndependent K v) : LinearIndependent R v :=
restrict_scalars ((faithfulSMul_iff_injective_smul_one R K).mp inferInstance) li
