R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
⊢ star a = a ∨ a = 0 ↔ star a = a
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
⊢ a ^ 2 = ↑(↑normSq a) ↔ a = ↑a.re
rw [← star_eq_self, ← star_mul_self, sq, mul_eq_mul_right_iff, eq_comm]
no goals
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
⊢ star a = a ∨ a = 0 ↔ star a = a
exact or_iff_left_of_imp fun ha ↦ ha.symm ▸ star_zero _