feat: generalize Matrix.PosDef.det_pos to complex matrices (#13744)

Also adds some missing `norm_cast` lemmas

Mathlib/Analysis/RCLike/Basic.lean

@@ -876,19 +876,32 @@ lemma nonpos_iff_exists_ofReal : z ≤ 0 ↔ ∃ x ≤ (0 : ℝ), x = z := by
 lemma neg_iff_exists_ofReal : z < 0 ↔ ∃ x < (0 : ℝ), x = z := by
   simp_rw [neg_iff (K := K), ext_iff (K := K)]; aesop
 
-@[simp]
+@[simp, norm_cast]
 lemma ofReal_le_ofReal {x y : ℝ} : (x : K) ≤ (y : K) ↔ x ≤ y := by
   rw [le_iff_re_im]
   simp
 
-@[simp]
+@[simp, norm_cast]
+lemma ofReal_lt_ofReal {x y : ℝ} : (x : K) < (y : K) ↔ x < y := by
+  rw [lt_iff_re_im]
+  simp
+
+@[simp, norm_cast]
 lemma ofReal_nonneg {x : ℝ} : 0 ≤ (x : K) ↔ 0 ≤ x := by
   rw [← ofReal_zero, ofReal_le_ofReal]
 
-@[simp]
+@[simp, norm_cast]
 lemma ofReal_nonpos {x : ℝ} : (x : K) ≤ 0 ↔ x ≤ 0 := by
   rw [← ofReal_zero, ofReal_le_ofReal]
 
+@[simp, norm_cast]
+lemma ofReal_pos {x : ℝ} : 0 < (x : K) ↔ 0 < x := by
+  rw [← ofReal_zero, ofReal_lt_ofReal]
+
+@[simp, norm_cast]
+lemma ofReal_lt_zero {x : ℝ} : (x : K) < 0 ↔ x < 0 := by
+  rw [← ofReal_zero, ofReal_lt_ofReal]
+
 /-- With `z ≤ w` iff `w - z` is real and nonnegative, `ℝ` and `ℂ` are star ordered rings.
 (That is, a star ring in which the nonnegative elements are those of the form `star z * z`.)
 

Mathlib/LinearAlgebra/Matrix/PosDef.lean

@@ -337,11 +337,11 @@ lemma eigenvalues_pos [DecidableEq n] {A : Matrix n n 𝕜}
   simp only [hA.1.eigenvalues_eq]
   exact hA.re_dotProduct_pos <| hA.1.eigenvectorBasis.orthonormal.ne_zero i
 
-theorem det_pos [DecidableEq n] {M : Matrix n n ℝ} (hM : M.PosDef) : 0 < det M := by
-   rw [hM.isHermitian.det_eq_prod_eigenvalues]
-   apply Finset.prod_pos
-   intro i _
-   exact hM.eigenvalues_pos i
+theorem det_pos [DecidableEq n] {M : Matrix n n 𝕜} (hM : M.PosDef) : 0 < det M := by
+  rw [hM.isHermitian.det_eq_prod_eigenvalues]
+  apply Finset.prod_pos
+  intro i _
+  simpa using hM.eigenvalues_pos i
 #align matrix.pos_def.det_pos Matrix.PosDef.det_pos
 
 end PosDef