Theorem: Matrix.PosDef.det_ne_zero (CvxLean/Lib/Math/LinearAlgebra/Matrix/PosDef.lean)

State before:
m : Type ?u.1418
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
⊢ M.det ≠ 0
Tactic:
rw [← Matrix.nondegenerate_iff_det_ne_zero]
State after:
m : Type ?u.1418
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
⊢ M.Nondegenerate

State before:
m : Type ?u.1418
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
⊢ M.Nondegenerate
Tactic:
intros v hv
State after:
m : Type ?u.1418
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
v : n → 𝕜
hv : ∀ (w : n → 𝕜), v ⬝ᵥ M.mulVec w = 0
⊢ v = 0

State before:
m : Type ?u.1418
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
v : n → 𝕜
hv : ∀ (w : n → 𝕜), v ⬝ᵥ M.mulVec w = 0
⊢ v = 0
Tactic:
have hv' := hv (star v)
State after:
m : Type ?u.1418
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
v : n → 𝕜
hv : ∀ (w : n → 𝕜), v ⬝ᵥ M.mulVec w = 0
hv' : v ⬝ᵥ M.mulVec (star v) = 0
⊢ v = 0

State before:
m : Type ?u.1418
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
v : n → 𝕜
hv : ∀ (w : n → 𝕜), v ⬝ᵥ M.mulVec w = 0
hv' : v ⬝ᵥ M.mulVec (star v) = 0
⊢ v = 0
Tactic:
rw [← star_eq_zero]
State after:
m : Type ?u.1418
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
v : n → 𝕜
hv : ∀ (w : n → 𝕜), v ⬝ᵥ M.mulVec w = 0
hv' : v ⬝ᵥ M.mulVec (star v) = 0
⊢ star v = 0

State before:
m : Type ?u.1418
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
v : n → 𝕜
hv : ∀ (w : n → 𝕜), v ⬝ᵥ M.mulVec w = 0
hv' : v ⬝ᵥ M.mulVec (star v) = 0
⊢ star v = 0
Tactic:
by_contra h
State after:
m : Type ?u.1418
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
v : n → 𝕜
hv : ∀ (w : n → 𝕜), v ⬝ᵥ M.mulVec w = 0
hv' : v ⬝ᵥ M.mulVec (star v) = 0
h : ¬star v = 0
⊢ False

State before:
m : Type ?u.1418
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
v : n → 𝕜
hv : ∀ (w : n → 𝕜), v ⬝ᵥ M.mulVec w = 0
hv' : v ⬝ᵥ M.mulVec (star v) = 0
h : ¬star v = 0
⊢ False
Tactic:
have := hM.2 (star v) h
State after:
m : Type ?u.1418
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
v : n → 𝕜
hv : ∀ (w : n → 𝕜), v ⬝ᵥ M.mulVec w = 0
hv' : v ⬝ᵥ M.mulVec (star v) = 0
h : ¬star v = 0
this : 0 < star (star v) ⬝ᵥ M.mulVec (star v)
⊢ False

State before:
m : Type ?u.1418
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
v : n → 𝕜
hv : ∀ (w : n → 𝕜), v ⬝ᵥ M.mulVec w = 0
hv' : v ⬝ᵥ M.mulVec (star v) = 0
h : ¬star v = 0
this : 0 < star (star v) ⬝ᵥ M.mulVec (star v)
⊢ False
Tactic:
simp [star_star, hv'] at this
State after:
no goals