# Pointwise operations of sets in a ring #

This file proves properties of pointwise operations of sets in a ring.

## Tags #

set multiplication, set addition, pointwise addition, pointwise multiplication, pointwise subtraction

source
@[simp]
theorem Set.smul_set_neg {α : Type u_1} {β : Type u_2} [Monoid α] [AddGroup β] [DistribMulAction α β] (a : α) (t : Set β) :
a • -t = -(a • t)
source
@[simp]
theorem Set.smul_neg {α : Type u_1} {β : Type u_2} [Monoid α] [AddGroup β] [DistribMulAction α β] (s : Set α) (t : Set β) :
s • -t = -(s • t)
source
theorem Set.add_smul_subset {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommMonoid β] [Module α β] (a b : α) (s : Set β) :
(a + b) • s ⊆ a • s + b • s
source
@[simp]
theorem Set.neg_smul_set {α : Type u_1} {β : Type u_2} [Ring α] [AddCommGroup β] [Module α β] (a : α) (t : Set β) :
-a • t = -(a • t)
source
@[simp]
theorem Set.neg_smul {α : Type u_1} {β : Type u_2} [Ring α] [AddCommGroup β] [Module α β] (s : Set α) (t : Set β) :
-s • t = -(s • t)