docstrings

Author: themathqueen

Mathlib/LinearAlgebra/Matrix/PosDef.lean

@@ -424,10 +424,12 @@ theorem PosSemidef.commute_iff [DecidableEq n] {A B : Matrix n n 𝕜}
       exact posSemidef_iff_isHermitian_and_spectrum_nonneg.mp
         (posSemidef_conjTranspose_mul_self _) |>.2
 
+/-- The matrix `vecMulVec a (star a)` is always positive semi-definite. -/
 theorem posSemidef_vecMulVec_self_star [StarOrderedRing R] (a : n → R) :
     (vecMulVec a (star a)).PosSemidef := by
   simp [vecMulVec_eq Unit, ← conjTranspose_replicateCol, posSemidef_self_mul_conjTranspose]
 
+/-- The matrix `vecMulVec (star a) a` is always postive semi-definite. -/
 theorem posSemidef_vecMulVec_star_self [StarOrderedRing R] (a : n → R) :
     (vecMulVec (star a) a).PosSemidef := by
   simp [vecMulVec_eq Unit, ← conjTranspose_replicateRow, posSemidef_conjTranspose_mul_self]
@@ -572,19 +574,27 @@ theorem mul_conjTranspose_self [StarOrderedRing R] [NoZeroDivisors R] (A : Matri
   classical
   simpa using mul_mul_conjTranspose_same .one hA
 
+/-- If `dotProduct · a` is injective, then `vecMulVec a (star a)` is positive definite.
+
+In a nontrivial commutative ring with nontrivial index, this is never positive definite
+(see `Matrix.not_posDef_vecMulVec`). -/
 theorem _root_.Matrix.posDef_vecMulVec_star [StarOrderedRing R] [NoZeroDivisors R] (a : n → R)
     (ha : Function.Injective (dotProduct · a)) :
     (vecMulVec a (star a)).PosDef := by
   simp only [vecMulVec_eq Unit, ← conjTranspose_replicateCol]
   exact mul_conjTranspose_self _ fun a b => by simp [← ha.eq_iff, funext_iff, vecMul]
 
+/-- If `dotProduct a` is injective, then `vecMulVec (star a) a` is positive definite.
+
+In a nontrivial commutative ring with nontrivial index, this is never positive definite
+(see `Matrix.not_posDef_vecMulVec`). -/
 theorem _root_.Matrix.posDef_star_vecMulVec [StarOrderedRing R] [NoZeroDivisors R] (a : n → R)
     (ha : Function.Injective (dotProduct a)) :
     (vecMulVec (star a) a).PosDef := by
   simp only [vecMulVec_eq Unit, ← conjTranspose_replicateRow]
   exact conjTranspose_mul_self _ fun a b => by simp [← ha.eq_iff, funext_iff, mulVec]
 
-/-- In a nontrivial commutative ⋆-ring with nontrivial index, the matrices
+/-- In a nontrivial commutative ring with nontrivial index, the matrices
 `vecMulVec a (star a)` and `vecMulVec (star a) a` are never positive definite. -/
 theorem _root_.Matrix.not_posDef_vecMulVec [Nontrivial n] [Nontrivial R'] (a : n → R') :
     ¬ (vecMulVec a (star a)).PosDef ∧ ¬ (vecMulVec (star a) a).PosDef := by