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

State before:
m : Type ?u.34280
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.IsHermitian
hMdet : IsUnit M.det
⊢ M⁻¹.IsHermitian
Tactic:
refine' (Matrix.inv_eq_right_inv _).symm
State after:
m : Type ?u.34280
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.IsHermitian
hMdet : IsUnit M.det
⊢ M * M⁻¹.conjTranspose = 1

State before:
m : Type ?u.34280
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.IsHermitian
hMdet : IsUnit M.det
⊢ M * M⁻¹.conjTranspose = 1
Tactic:
rw [conjTranspose_nonsing_inv, hM.eq, mul_nonsing_inv _ hMdet]
State after:
no goals