Theorem: LDL.det_lower (CvxLean/Lib/Math/LinearAlgebra/Matrix/LDL.lean)

State before:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
⊢ (lower hS).det = 1
Tactic:
simp [lower]
State after:
no goals