Theorem: Matrix.LogDetAtom.feasibility_exp (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
⊢ LDL.diagEntries hA i ≤ (LDL.diag hA * (LDL.lower hA).transpose).diag i
Tactic:
simp [LDL.diag]
State after:
no goals