Theorem: Matrix.PosSemidef.det_nonneg (CvxLean/Lib/Math/LinearAlgebra/Matrix/PosDef.lean)

State before:
m : Type ?u.340
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.352
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
M : Matrix n n ℝ
hM : M.PosSemidef
inst✝ : DecidableEq n
⊢ 0 ≤ M.det
Tactic:
rw [hM.1.det_eq_prod_eigenvalues]
State after:
m : Type ?u.340
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.352
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
M : Matrix n n ℝ
hM : M.PosSemidef
inst✝ : DecidableEq n
⊢ 0 ≤ Finset.univ.prod fun i => ↑(⋯.eigenvalues i)

State before:
m : Type ?u.340
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.352
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
M : Matrix n n ℝ
hM : M.PosSemidef
inst✝ : DecidableEq n
⊢ 0 ≤ Finset.univ.prod fun i => ↑(⋯.eigenvalues i)
Tactic:
apply Finset.prod_nonneg
State after:
case h0
m : Type ?u.340
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.352
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
M : Matrix n n ℝ
hM : M.PosSemidef
inst✝ : DecidableEq n
⊢ ∀ i ∈ Finset.univ, 0 ≤ ↑(⋯.eigenvalues i)

State before:
case h0
m : Type ?u.340
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.352
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
M : Matrix n n ℝ
hM : M.PosSemidef
inst✝ : DecidableEq n
⊢ ∀ i ∈ Finset.univ, 0 ≤ ↑(⋯.eigenvalues i)
Tactic:
intros i _hi
State after:
case h0
m : Type ?u.340
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.352
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
M : Matrix n n ℝ
hM : M.PosSemidef
inst✝ : DecidableEq n
i : n
_hi : i ∈ Finset.univ
⊢ 0 ≤ ↑(⋯.eigenvalues i)

State before:
case h0
m : Type ?u.340
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.352
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
M : Matrix n n ℝ
hM : M.PosSemidef
inst✝ : DecidableEq n
i : n
_hi : i ∈ Finset.univ
⊢ 0 ≤ ↑(⋯.eigenvalues i)
Tactic:
apply eigenvalues_nonneg hM
State after:
no goals