fin_cons' — Mathlib

English

If v is LI and f,g are vector coefficients with equal sums in a LI combination, then the coefficients are equal coordinatewise.

Русский

Если v линейно независимо и сумма с коэффициентами f и g совпадает, то коэффициенты равны по каждому индексу.

LaTeX

$$$\\text{LinearIndependent } R\\ v \\rightarrow \\big(\\sum_i f_i v_i = \\sum_i g_i v_i\\big) \\Rightarrow \\forall i,\\ f_i = g_i$$$

Lean4

/-- See `LinearIndependent.fin_cons` for a family of elements in a vector space. -/
theorem fin_cons' {m : ℕ} (x : M) (v : Fin m → M) (hli : LinearIndependent R v)
    (x_ortho : ∀ (c : R) (y : Submodule.span R (Set.range v)), c • x + y = (0 : M) → c = 0) :
    LinearIndependent R (Fin.cons x v : Fin m.succ → M) :=
  by
  rw [Fintype.linearIndependent_iff] at hli ⊢
  rintro g total_eq j
  simp_rw [Fin.sum_univ_succ, Fin.cons_zero, Fin.cons_succ] at total_eq
  have : g 0 = 0 := by
    refine x_ortho (g 0) ⟨∑ i : Fin m, g i.succ • v i, ?_⟩ total_eq
    exact sum_mem fun i _ => smul_mem _ _ (subset_span ⟨i, rfl⟩)
  rw [this, zero_smul, zero_add] at total_eq
  exact Fin.cases this (hli _ total_eq) j

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