wInner_one_const_right — Mathlib

English

If for a family f: κ → ι → 𝕜 we have f(k) ≠ 0 for all k and the Gram matrix ⟪f(k1), f(k2)⟫ is zero for k1 ≠ k2, then f is linearly independent.

Русский

Если каждый f(k) ≠ 0 и ⟪f(k1), f(k2)⟫ = 0 при k1 ≠ k2, то семейство линейно независимo.

LaTeX

$$hf : ∀ k, f k ≠ 0 ∧ hinner : Pairwise (k1 ≠ k2 → ⟪f k1, f k2⟫ = 0) → LinearIndependent 𝕜 f$$

Lean4

@[simp]
theorem wInner_one_const_right (f : ι → 𝕜) (a : 𝕜) : ⟪f, const _ a⟫_[𝕜] = a * (∑ i, conj (f i)) := by
  simp [wInner_one_eq_sum, mul_sum]

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