no goals
R : Type u_2
A : Type u_1
inst✝⁷ : Semiring R
inst✝⁶ : StarSemigroup R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : A
hx : IsSelfAdjoint x
⊢ ↑(↑(skewAdjointPart R) x) = ↑0
rw [skewAdjointPart_apply_coe, hx.star_eq, sub_self, smul_zero, ZeroMemClass.coe_zero]