Theorem: LDL.lower_diagonal (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
i : n
⊢ lower hS i i = 1
Tactic:
simpa using
  diag_inv_mul_diag_eq_one_of_lowerTriangular (lowerTriangular_lower hS) i
State after:
no goals