no goals
R : Type u_1
A : Type ?u.52269
inst✝¹ : Semifield R
inst✝ : StarRing R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ IsSelfAdjoint (x / y)
simp only [isSelfAdjoint_iff, star_div', hx.star_eq, hy.star_eq]