Theorem: Matrix.IsHermitian.one_add (CvxLean/Lib/Math/Subadditivity.lean)

State before:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.IsHermitian
⊢ (1 + A).IsHermitian
Tactic:
dsimp [IsHermitian]
State after:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.IsHermitian
⊢ (1 + A).conjTranspose = 1 + A

State before:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.IsHermitian
⊢ (1 + A).conjTranspose = 1 + A
Tactic:
rw [IsHermitian.add _ hA]
State after:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.IsHermitian
⊢ IsHermitian 1

State before:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.IsHermitian
⊢ IsHermitian 1
Tactic:
simp
State after:
no goals