R : Type u_1
A : Type ?u.113647
inst✝¹ : Ring R
inst✝ : StarRing R
x : R
hx : star x = -x
⊢ Commute (star x) x
R : Type u_1
A : Type ?u.113647
inst✝¹ : Ring R
inst✝ : StarRing R
x : R
hx : x ∈ skewAdjoint R
⊢ Commute (star x) x
simp only [mem_iff] at hx
no goals
R : Type u_1
A : Type ?u.113647
inst✝¹ : Ring R
inst✝ : StarRing R
x : R
hx : star x = -x
⊢ Commute (star x) x
simp only [hx, Commute.neg_left, Commute.refl]