no goals
R : Type u_1
A : Type ?u.38508
inst✝¹ : CommSemigroup R
inst✝ : StarSemigroup R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ IsSelfAdjoint (x * y)
simp only [isSelfAdjoint_iff, star_mul', hx.star_eq, hy.star_eq]