no goals
S : Type ?u.321798
T : Type ?u.321801
R : Type u_1
inst✝² : CommRing R
c₁✝ c₂✝ r x y z : R
a✝ b c : ℍ[R,c₁✝,c₂✝]
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
c₁ c₂ : R
a : ℍ[R,c₁,c₂]
⊢ star a = -a ↔ a.re = 0
simp [QuaternionAlgebra.ext_iff, eq_neg_iff_add_eq_zero]