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

State before:
m : Type ?u.36361
n : Type u_1
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
x : n → 𝕜
M : Matrix n n 𝕜
hM : M.IsHermitian
⊢ star (star x ⬝ᵥ M.mulVec x) = star x ⬝ᵥ M.mulVec x
Tactic:
nth_rewrite 1 [star_dotProduct, star_mulVec]
State after:
m : Type ?u.36361
n : Type u_1
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
x : n → 𝕜
M : Matrix n n 𝕜
hM : M.IsHermitian
⊢ star (star (star x ᵥ* M.conjTranspose ⬝ᵥ x)) = star x ⬝ᵥ M.mulVec x

State before:
m : Type ?u.36361
n : Type u_1
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
x : n → 𝕜
M : Matrix n n 𝕜
hM : M.IsHermitian
⊢ star (star (star x ᵥ* M.conjTranspose ⬝ᵥ x)) = star x ⬝ᵥ M.mulVec x
Tactic:
rw [star_star, dotProduct_mulVec, hM.eq]
State after:
no goals