feat(Analysis/InnerProductSpace): generalized determinant of a rectangle matrix / linear map

Author: wwylele

Mathlib.lean

@@ -1963,6 +1963,7 @@ public import Mathlib.Analysis.InnerProductSpace.LinearMap
 public import Mathlib.Analysis.InnerProductSpace.LinearPMap
 public import Mathlib.Analysis.InnerProductSpace.MeanErgodic
 public import Mathlib.Analysis.InnerProductSpace.MulOpposite
+public import Mathlib.Analysis.InnerProductSpace.NormDet
 public import Mathlib.Analysis.InnerProductSpace.NormPow
 public import Mathlib.Analysis.InnerProductSpace.OfNorm
 public import Mathlib.Analysis.InnerProductSpace.Orientation

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,12 @@ 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 := by
+  apply linearIndependent_of_posDef_gram
+  simpa [(Matrix.posSemidef_gram _ _).posDef_iff_isUnit, Matrix.isUnit_iff_isUnit_det] using h
+
 end SemiInnerProductSpace
 
 section NormedInnerProductSpace