linearIndependent_of_posDef_gram — Mathlib

English

If the Gram matrix of v is positive definite, then v is linearly independent.

Русский

Если граммова матрица вектора линейно независимая, то вектор линейно независим.

LaTeX

$$$ (\text{gram } 𝕜 v).PosDef \Rightarrow \text{LinearIndependent } 𝕜 v $$$

Lean4

/-- In a normed space, positive definiteness of `gram 𝕜 v` implies linear independence of `v`. -/
theorem linearIndependent_of_posDef_gram {v : n → E} (h_gram : PosDef (gram 𝕜 v)) : LinearIndependent 𝕜 v :=
  by
  rw [Fintype.linearIndependent_iff]
  intro y hy
  obtain ⟨h1, h2⟩ := h_gram
  specialize h2 y
  simp_all [star_dotProduct_gram_mulVec]

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