∀ {R : Type u_2} {A : Type u_1} [inst : Star R] [TrivialStar R] [inst_2 : AddGroup A] [inst_3 : StarAddMonoid A]
  [inst_4 : SMul R A] [StarModule R A] (r : R) (x : ↥(selfAdjoint A)), IsSelfAdjoint (r • ↑x)