∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [inst : Star R] [inst_1 : Star α] [inst_2 : SMul R α]
  [StarModule R α] (c : R) (M : Matrix m n α), (c • M).conjTranspose = star c • M.conjTranspose