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

@[simp]

theorem Set.smul_set_neg {α : Type u_1} {β : Type u_2} [Monoid α] [AddGroup β] [DistribMulAction α β] (a : α) (t : Set β) : a • -t = -(a • t)

@[simp]

theorem Set.smul_neg {α : Type u_1} {β : Type u_2} [Monoid α] [AddGroup β] [DistribMulAction α β] (s : Set α) (t : Set β) : s • -t = -(s • t)

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

@[simp]

theorem Set.neg_smul_set {α : Type u_1} {β : Type u_2} [Ring α] [AddCommGroup β] [Module α β] (a : α) (t : Set β) : -a • t = -(a • t)

@[simp]

theorem Set.neg_smul {α : Type u_1} {β : Type u_2} [Ring α] [AddCommGroup β] [Module α β] (s : Set α) (t : Set β) : -s • t = -(s • t)