linearIndependent_of_ne_zero_of_wInner_cWeight_eq_zero

English

Analogous to the previous, but with cWeight inner products; if f_k ≠ 0 and ⟪f k1, f k2⟫_{cWeight} = 0 for k1 ≠ k2, then f is linearly independent.

Русский

Аналогично, но с внутренним произведением по весу cWeight; если f_k ≠ 0 и ⟪f k1, f k2⟫_{cWeight} = 0 для k1 ≠ k2, тогда f линейно независим.

LaTeX

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

Lean4

theorem linearIndependent_of_ne_zero_of_wInner_cWeight_eq_zero {f : κ → ι → 𝕜} (hf : ∀ k, f k ≠ 0)
    (hinner : Pairwise fun k₁ k₂ ↦ ⟪f k₁, f k₂⟫ₙ_[𝕜] = 0) : LinearIndependent 𝕜 f :=
  by
  cases isEmpty_or_nonempty ι
  · have : IsEmpty κ := ⟨fun k ↦ hf k <| Subsingleton.elim ..⟩
    exact linearIndependent_empty_type
  ·
    exact
      linearIndependent_of_ne_zero_of_wInner_one_eq_zero hf <| by
        simpa [wInner_cWeight_eq_smul_wInner_one, ← NNRat.cast_smul_eq_nnqsmul 𝕜] using hinner

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