English
Fix an index i and a coefficient function c: ι → R with c(i) = 0. Then the linear independence of the family v is unchanged if one replaces v by the family v + (c · • v i), i.e., the j-th component becomes v(j) + c(j) v(i).
Русский
Пусть существует индекс i и функция коэффициентов c: ι → R такая, что c(i) = 0. Тогда линейная независимость семейства v не меняется при замене v на v + (c · • v i), т.е. j-ая компонента становится v(j) + c(j) v(i).
LaTeX
$$$$\\operatorname{LinearIndependent}_R\\big(v + (c \\cdot \\bullet v_i)\\big) \\\\iff \\operatorname{LinearIndependent}_R(v)\\quad \\text{при } c(i)=0.$$$$
Lean4
theorem linearIndependent_add_smul_iff {c : ι → R} {i : ι} (h₀ : c i = 0) :
LinearIndependent R (v + (c · • v i)) ↔ LinearIndependent R v := by
simp [linearIndependent_iff_injective_finsuppLinearCombination,
← Finsupp.linearCombination_comp_addSingleEquiv i c h₀]
