Theorem: LDL.det_lowerInv (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
⊢ (lowerInv hS).det = 1
Tactic:
have h := det_of_lowerTriangular (lowerInv hS) (by apply lowerInv_triangular)
State after:
𝕜 : 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
h : (lowerInv hS).det = Finset.univ.prod fun i => lowerInv hS i i
⊢ (lowerInv hS).det = 1

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
h : (lowerInv hS).det = Finset.univ.prod fun i => lowerInv hS i i
⊢ (lowerInv hS).det = 1
Tactic:
rw [h, Finset.prod_eq_one]
State after:
𝕜 : 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
h : (lowerInv hS).det = Finset.univ.prod fun i => lowerInv hS i i
⊢ ∀ x ∈ Finset.univ, lowerInv hS x x = 1

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
h : (lowerInv hS).det = Finset.univ.prod fun i => lowerInv hS i i
⊢ ∀ x ∈ Finset.univ, lowerInv hS x x = 1
Tactic:
intros
State after:
𝕜 : 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
h : (lowerInv hS).det = Finset.univ.prod fun i => lowerInv hS i i
x✝ : n
a✝ : x✝ ∈ Finset.univ
⊢ lowerInv hS x✝ x✝ = 1

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
h : (lowerInv hS).det = Finset.univ.prod fun i => lowerInv hS i i
x✝ : n
a✝ : x✝ ∈ Finset.univ
⊢ lowerInv hS x✝ x✝ = 1
Tactic:
rw [lowerInv_diagonal]
State after:
no goals

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
⊢ (lowerInv hS).BlockTriangular ⇑OrderDual.toDual
Tactic:
apply lowerInv_triangular
State after:
no goals