generalize more stuf

Author: themathqueen

Mathlib/Analysis/Matrix/Order.lean

@@ -175,18 +175,6 @@ theorem posSemidef_iff_isHermitian_and_spectrum_nonneg [DecidableEq n] {A : Matr
     intro i
     simpa [h1.spectrum_eq_image_range] using @h2 (h1.eigenvalues i)
 
-/-- A positive semi-definite matrix is positive definite if and only if it is invertible. -/
-@[grind =]
-theorem PosSemidef.posDef_iff_isUnit [DecidableEq n] {x : Matrix n n 𝕜}
-    (hx : x.PosSemidef) : x.PosDef ↔ IsUnit x := by
-  refine ⟨fun h => h.isUnit, fun h => .of_dotProduct_mulVec_pos hx.1 fun v hv => ?_⟩
-  obtain ⟨y, rfl⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hx.nonneg
-  simp_rw [dotProduct_mulVec, ← vecMul_vecMul, star_eq_conjTranspose, ← star_mulVec,
-    ← dotProduct_mulVec, dotProduct_star_self_pos_iff]
-  contrapose hv
-  rw [← map_eq_zero_iff (f := (yᴴ * y).mulVecLin) (mulVec_injective_iff_isUnit.mpr h),
-    mulVecLin_apply, ← mulVec_mulVec, hv, mulVec_zero]
-
 theorem isStrictlyPositive_iff_posDef [DecidableEq n] {x : Matrix n n 𝕜} :
     IsStrictlyPositive x ↔ x.PosDef :=
   ⟨fun h => h.nonneg.posSemidef.posDef_iff_isUnit.mpr h.isUnit,
@@ -196,9 +184,6 @@ 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]
 
 section kronecker
 

Mathlib/LinearAlgebra/Matrix/PosDef.lean

@@ -496,6 +496,23 @@ theorem mul_conjTranspose_self [StarOrderedRing R] [NoZeroDivisors R] (A : Matri
   classical
   simpa using mul_mul_conjTranspose_same .one hA
 
+lemma mulVec_injective {M : Matrix n n R} (hM : M.PosDef) : Function.Injective M.mulVec := by
+  intro _ _ hxy; by_contra h
+  simpa [mulVec_sub, hxy] using hM.dotProduct_mulVec_pos (sub_ne_zero_of_ne h)
+
+lemma _root_.Matrix.posDef_iff_posSemidef_and_mulVec_injective [StarOrderedRing R']
+    [NoZeroDivisors R'] {A : Matrix n n R'} :
+    PosDef A ↔ A.PosSemidef ∧ Function.Injective A.mulVec := by
+  refine ⟨fun hA ↦ ⟨hA.posSemidef, hA.mulVec_injective⟩, fun ⟨hA, hA'⟩ ↦ ?_⟩
+  refine posDef_iff_dotProduct_mulVec.mpr ⟨hA.isHermitian, fun x hx ↦ lt_of_le_of_ne' ?_ ?_⟩
+  · exact hA.dotProduct_mulVec_nonneg x
+  simpa [hA.dotProduct_mulVec_zero_iff, hx] using hA'.eq_iff (a := x) (b := 0)
+
+lemma _root_.Matrix.PosSemidef.posDef_iff_mulVec_injective [StarOrderedRing R']
+    [NoZeroDivisors R'] {A : Matrix n n R'} (hA : A.PosSemidef) :
+    PosDef A ↔ Function.Injective A.mulVec := by
+  simp [posDef_iff_posSemidef_and_mulVec_injective, hA]
+
 theorem of_toQuadraticForm' {R : Type*} [CommRing R] [PartialOrder R] [StarRing R] [TrivialStar R]
     [DecidableEq n] {M : Matrix n n R} (hM : M.IsSymm)
     (hMq : M.toQuadraticForm'.PosDef) : M.PosDef := by
@@ -554,12 +571,8 @@ theorem det_pos [DecidableEq n] [Nontrivial R'] [IsOrderedRing R'] [PosMulReflec
 section Field
 variable {K : Type*} [Field K] [PartialOrder K] [StarRing K]
 
-theorem isUnit [DecidableEq n] {M : Matrix n n K} (hM : M.PosDef) : IsUnit M := by
-  by_contra h
-  obtain ⟨a, ha, ha2⟩ : ∃ a ≠ 0, M *ᵥ a = 0 := by
-    obtain ⟨a, b, ha⟩ := Function.not_injective_iff.mp <| mulVec_injective_iff_isUnit.not.mpr h
-    exact ⟨a - b, by simp [sub_eq_zero, ha, mulVec_sub]⟩
-  simpa [ha2] using hM.dotProduct_mulVec_pos ha
+theorem isUnit [DecidableEq n] {M : Matrix n n K} (hM : M.PosDef) : IsUnit M :=
+  mulVec_injective_iff_isUnit.mp (mulVec_injective hM)
 
 protected theorem inv [DecidableEq n] {M : Matrix n n K} (hM : M.PosDef) : M⁻¹.PosDef := by
   have := hM.mul_mul_conjTranspose_same (B := M⁻¹) ?_
@@ -574,6 +587,16 @@ theorem _root_.Matrix.posDef_inv_iff [DecidableEq n] {M : Matrix n n K} :
     letI := (Matrix.isUnit_nonsing_inv_iff.1 <| h.isUnit).invertible
     Matrix.inv_inv_of_invertible M ▸ h.inv, (·.inv)⟩
 
+/-- A positive semi-definite matrix is positive definite if and only if it is invertible. -/
+@[grind =]
+theorem _root_.Matrix.PosSemidef.posDef_iff_isUnit [DecidableEq n] [StarOrderedRing K]
+    {A : Matrix n n K} (hA : A.PosSemidef) : A.PosDef ↔ IsUnit A := by
+  simp [hA.posDef_iff_mulVec_injective, mulVec_injective_iff_isUnit]
+
+lemma _root_.Matrix.PosSemidef.posDef_iff_det_ne_zero [DecidableEq n] [StarOrderedRing K]
+    {A : Matrix n n K} (hA : A.PosSemidef) : A.PosDef ↔ A.det ≠ 0 := by
+  simp [hA.posDef_iff_isUnit, isUnit_iff_isUnit_det]
+
 end Field
 
 section conjugate