∀ (R : Type u_2) (A : Type u_1) [inst : Semiring R] [inst_1 : StarMul R] [TrivialStar R] [inst_3 : AddCommGroup A]
  [inst_4 : Module R A] [inst_5 : StarAddMonoid A] [StarModule R A] (r : R) {x : A},
  x ∈ skewAdjoint A → r • x ∈ skewAdjoint A