R : Type u_1
A : Type ?u.59390
inst✝¹ : AddGroup R
inst✝ : StarAddMonoid R
x : R
⊢ x ∈ (selfAdjoint R).toAddSubmonoid.toAddSubsemigroup.carrier ↔ star x = x
R : Type u_1
A : Type ?u.59390
inst✝¹ : AddGroup R
inst✝ : StarAddMonoid R
x : R
⊢ x ∈ selfAdjoint R ↔ star x = x
rw [← AddSubgroup.mem_carrier]
no goals
R : Type u_1
A : Type ?u.59390
inst✝¹ : AddGroup R
inst✝ : StarAddMonoid R
x : R
⊢ x ∈ (selfAdjoint R).toAddSubmonoid.toAddSubsemigroup.carrier ↔ star x = x
exact Iff.rfl