linearIndependent_of_ne_zero_of_wInner_one_eq_zero

English

If a family f_k of nonzero vectors has pairwise zero unit-weight inner products, then it is linearly independent.

Русский

Если семейство ненулевых векторов имеет попарно нулевые единичные внутренние произведения, то оно линейно независимо.

LaTeX

$$hf : ∀ k, f k ≠ 0 → (Pairwise fun k₁ k₂ ↦ ⟪f k₁, f k₂⟫_𝕜 = 0) → LinearIndependent 𝕜 f$$

Lean4

theorem linearIndependent_of_ne_zero_of_wInner_one_eq_zero {f : κ → ι → 𝕜} (hf : ∀ k, f k ≠ 0)
    (hinner : Pairwise fun k₁ k₂ ↦ ⟪f k₁, f k₂⟫_[𝕜] = 0) : LinearIndependent 𝕜 f :=
  by
  simp_rw [wInner_one_eq_inner] at hinner
  have := linearIndependent_of_ne_zero_of_inner_eq_zero ?_ hinner
  exacts [this, hf]

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