theorem Set.singleton_mul' {α : Type u_1} [Mul α] (a : α) (s : Set α) : {a} * s = a • s

theorem Set.singleton_add' {α : Type u_1} [Add α] (a : α) (s : Set α) : {a} + s = a +ᵥ s

theorem Set.mul_singleton' {α : Type u_1} [Mul α] (s : Set α) (a : α) : s * {a} = MulOpposite.op a • s

theorem Set.add_singleton' {α : Type u_1} [Add α] (s : Set α) (a : α) : s + {a} = AddOpposite.op a +ᵥ s