no goals
S : Type ?u.319486
T : Type ?u.319489
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 = ↑a.re
simp [QuaternionAlgebra.ext_iff, neg_eq_iff_add_eq_zero, add_self_eq_zero]