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

theorem Set.zero_mem_smul_set_iff {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommMonoid β] [Module α β] [IsDomain α] [Module.IsTorsionFree α β] {a : α} {t : Set β} (ha : a ≠ 0) : 0 ∈ a • t ↔ 0 ∈ t

theorem Set.zero_mem_smul_iff {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommMonoid β] [Module α β] [IsDomain α] [Module.IsTorsionFree α β] {s : Set α} {t : Set β} : 0 ∈ s • t ↔ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

@[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)