eq_coords_of_eq — Mathlib

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))

Похожие утверждения