# Pointwise operations of sets in a group with zero #

This file proves properties of pointwise operations of sets in a group with zero.

## Tags #

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

Note that `Set` is not a `MulZeroClass` because `0 * ∅ ≠ 0`.

source
theorem Set.mul_zero_subset {α : Type u_1} [MulZeroClass α] (s : Set α) :
s * 0 ⊆ 0
source
theorem Set.zero_mul_subset {α : Type u_1} [MulZeroClass α] (s : Set α) :
0 * s ⊆ 0
source
theorem Set.Nonempty.mul_zero {α : Type u_1} [MulZeroClass α] {s : Set α} (hs : s.Nonempty) :
s * 0 = 0
source
theorem Set.Nonempty.zero_mul {α : Type u_1} [MulZeroClass α] {s : Set α} (hs : s.Nonempty) :
0 * s = 0
source
theorem Set.div_zero_subset {α : Type u_1} [GroupWithZero α] (s : Set α) :
s / 0 ⊆ 0
source
theorem Set.zero_div_subset {α : Type u_1} [GroupWithZero α] (s : Set α) :
0 / s ⊆ 0
source
theorem Set.Nonempty.div_zero {α : Type u_1} [GroupWithZero α] {s : Set α} (hs : s.Nonempty) :
s / 0 = 0
source
theorem Set.Nonempty.zero_div {α : Type u_1} [GroupWithZero α] {s : Set α} (hs : s.Nonempty) :
0 / s = 0
source
@[simp]
theorem Set.inv_zero {α : Type u_1} [GroupWithZero α] :
0⁻¹ = 0