no goals
𝕜 : Type u_1
E : Type ?u.431471
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x y : F
⊢ ↑im (inner x y) = -↑im (inner y x)
rw [← inner_conj_symm, conj_im]