English
If v is LI and sums equal, then coordinates are equal for all indices.
Русский
Если v линейно независимо и суммы равны, тогда координаты по всем индексам совпадают.
LaTeX
$$$\\text{EqCoords}$: \n\\forall f,g:\\, \\sum_i f_i v_i = \\sum_i g_i v_i \\Rightarrow \\forall i,\\ f_i=g_i$$$
Lean4
/-- If `∑ i, f i • v i = ∑ i, g i • v i`, then for all `i`, `f i = g i`. -/
theorem eq_coords_of_eq [Fintype ι] {v : ι → M} (hv : LinearIndependent R v) {f : ι → R} {g : ι → R}
(heq : ∑ i, f i • v i = ∑ i, g i • v i) (i : ι) : f i = g i :=
by
rw [← sub_eq_zero, ← sum_sub_distrib] at heq
simp_rw [← sub_smul] at heq
exact sub_eq_zero.mp ((linearIndependent_iff'.mp hv) univ (fun i ↦ f i - g i) heq i (mem_univ i))