∀ {R : Type u_3} {A : Type u_4} [inst : SMul R A] [inst_1 : Star R] [inst_2 : Star A] [inst_3 : Mul A] [StarModule R A]
  [SMulCommClass R A A] [IsScalarTower R A A] (r : R) (a : A) [ha : IsStarNormal a], IsStarNormal (r • a)