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

State before:
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
n : Type u_1
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
⊢ (lowerInv hS).lowerTriangular
Tactic:
apply lowerInv_triangular
State after:
no goals