case a
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(↑ℑ (I • a)) = ↑(↑ℜ a)
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑ℑ (I • a) = ↑ℜ a
ext
case a
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ 2⁻¹ • -I • (I • a - star (I • a)) = 2⁻¹ • (a + star a)
case a
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(↑ℑ (I • a)) = ↑(↑ℜ a)
rw [realPart_apply_coe, imaginaryPart_apply_coe, smul_comm]
no goals
case a
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ 2⁻¹ • -I • (I • a - star (I • a)) = 2⁻¹ • (a + star a)
simp [←smul_assoc]