A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(↑(selfAdjointPart ℝ) a) = 2⁻¹ • (a + star a)
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(↑ℜ a) = 2⁻¹ • (a + star a)
unfold realPart
no goals
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(↑(selfAdjointPart ℝ) a) = 2⁻¹ • (a + star a)
simp only [selfAdjointPart_apply_coe, invOf_eq_inv]