feat(Analysis/InnerProductSpace): Gram matrix det ≠ 0 iff input vectors are independent (#37918)

Small lemma extracted from #37295. Convenient for talking about the determinant directly without detour through Pos(Semi)def

Author: wwylele

Mathlib/Analysis/InnerProductSpace/GramMatrix.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Analysis.InnerProductSpace.Basic
 public import Mathlib.Analysis.InnerProductSpace.PiL2
 public import Mathlib.LinearAlgebra.Matrix.PosDef
+import Mathlib.Analysis.Matrix.Order
 
 /-! # Gram Matrices
 
@@ -95,6 +96,11 @@ theorem linearIndependent_of_posDef_gram {v : n → E} (h_gram : PosDef (gram 
   have := h_gram.dotProduct_mulVec_pos (x := y)
   simp_all [star_dotProduct_gram_mulVec]
 
+omit [Finite n] in
+theorem linearIndependent_of_det_gram_ne_zero [Fintype n] [DecidableEq n] {v : n → E}
+    (h : (gram 𝕜 v).det ≠ 0) : LinearIndependent 𝕜 v :=
+  linearIndependent_of_posDef_gram <| (posSemidef_gram 𝕜 v).posDef_iff_det_ne_zero.mpr h
+
 end SemiInnerProductSpace
 
 section NormedInnerProductSpace
@@ -116,6 +122,11 @@ theorem posDef_gram_iff_linearIndependent {v : n → E} :
     PosDef (gram 𝕜 v) ↔ LinearIndependent 𝕜 v :=
   ⟨linearIndependent_of_posDef_gram, posDef_gram_of_linearIndependent⟩
 
+omit [Finite n] in
+theorem det_gram_ne_zero_iff_linearIndependent [Fintype n] [DecidableEq n] {v : n → E} :
+    (gram 𝕜 v).det ≠ 0 ↔ LinearIndependent 𝕜 v := by
+  rw [← posDef_gram_iff_linearIndependent, (posSemidef_gram 𝕜 v).posDef_iff_det_ne_zero]
+
 omit [Finite n] in
 theorem gram_eq_conjTranspose_mul {ι : Type*} [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (v : n → E) :
     letI m := of fun i j ↦ b.repr (v j) i

Mathlib/Analysis/Matrix/Order.lean

@@ -196,6 +196,10 @@ alias ⟨IsStrictlyPositive.posDef, PosDef.isStrictlyPositive⟩ := isStrictlyPo
 
 attribute [aesop safe forward (rule_sets := [CStarAlgebra])] PosDef.isStrictlyPositive
 
+lemma PosSemidef.posDef_iff_det_ne_zero [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.PosSemidef) :
+    A.PosDef ↔ A.det ≠ 0 := by
+  simp [hA.posDef_iff_isUnit, isUnit_iff_isUnit_det]
+
 @[deprecated IsStrictlyPositive.commute_iff (since := "2025-09-26")]
 theorem PosDef.commute_iff {A B : Matrix n n 𝕜} (hA : A.PosDef) (hB : B.PosDef) :
     Commute A B ↔ (A * B).PosDef := by