no goals
R : Type u_1
A : Type ?u.6762
inst✝¹ : AddMonoid R
inst✝ : StarAddMonoid R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ IsSelfAdjoint (x + y)
simp only [isSelfAdjoint_iff, star_add, hx.star_eq, hy.star_eq]