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