A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(↑(LinearMap.comp skewAdjoint.negISMul (skewAdjointPart ℝ)) a) = -I • 2⁻¹ • (a - star a)
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(↑ℑ a) = -I • 2⁻¹ • (a - star a)
unfold imaginaryPart
no goals
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(↑(LinearMap.comp skewAdjoint.negISMul (skewAdjointPart ℝ)) a) = -I • 2⁻¹ • (a - star a)
simp only [LinearMap.coe_comp, Function.comp_apply, skewAdjoint.negISMul_apply_coe,
  skewAdjointPart_apply_coe, invOf_eq_inv, neg_smul]