Theorem: Matrix.LDL.diagEntries_pos (CvxLean/Lib/Math/LogDet.lean)

State before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A✝ : Matrix n n ℝ
hA✝ : A✝.PosDef
A : Matrix n n ℝ
hA : A.PosDef
i : n
⊢ 0 < LDL.diagEntries hA i
Tactic:
have : (LDL.lowerInv hA).det ≠ 0 := by simp [LDL.det_lowerInv hA]
State after:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A✝ : Matrix n n ℝ
hA✝ : A✝.PosDef
A : Matrix n n ℝ
hA : A.PosDef
i : n
this : (LDL.lowerInv hA).det ≠ 0
⊢ 0 < LDL.diagEntries hA i

State before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A✝ : Matrix n n ℝ
hA✝ : A✝.PosDef
A : Matrix n n ℝ
hA : A.PosDef
i : n
this : (LDL.lowerInv hA).det ≠ 0
⊢ 0 < LDL.diagEntries hA i
Tactic:
have : LDL.lowerInv hA i ≠ 0 := fun h =>
  this (Matrix.det_eq_zero_of_row_eq_zero i (λ j => congr_fun h j))
State after:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A✝ : Matrix n n ℝ
hA✝ : A✝.PosDef
A : Matrix n n ℝ
hA : A.PosDef
i : n
this✝ : (LDL.lowerInv hA).det ≠ 0
this : LDL.lowerInv hA i ≠ 0
⊢ 0 < LDL.diagEntries hA i

State before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A✝ : Matrix n n ℝ
hA✝ : A✝.PosDef
A : Matrix n n ℝ
hA : A.PosDef
i : n
this✝ : (LDL.lowerInv hA).det ≠ 0
this : LDL.lowerInv hA i ≠ 0
⊢ 0 < LDL.diagEntries hA i
Tactic:
exact hA.2 (LDL.lowerInv hA i) this
State after:
no goals

State before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A✝ : Matrix n n ℝ
hA✝ : A✝.PosDef
A : Matrix n n ℝ
hA : A.PosDef
i : n
⊢ (LDL.lowerInv hA).det ≠ 0
Tactic:
simp [LDL.det_lowerInv hA]
State after:
no goals