Pointwise operations of finsets in a group with zero

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

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

theorem Finset.mul_zero_subset {α : Type u_1} [DecidableEq α] [MulZeroClass α] (s : Finset α) : s * 0 ⊆ 0

theorem Finset.zero_mul_subset {α : Type u_1} [DecidableEq α] [MulZeroClass α] (s : Finset α) : 0 * s ⊆ 0

theorem Finset.Nonempty.mul_zero {α : Type u_1} [DecidableEq α] [MulZeroClass α] {s : Finset α} (hs : s.Nonempty) : s * 0 = 0

theorem Finset.Nonempty.zero_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] {s : Finset α} (hs : s.Nonempty) : 0 * s = 0

theorem Finset.div_zero_subset {α : Type u_1} [GroupWithZero α] [DecidableEq α] (s : Finset α) : s / 0 ⊆ 0

theorem Finset.zero_div_subset {α : Type u_1} [GroupWithZero α] [DecidableEq α] (s : Finset α) : 0 / s ⊆ 0

theorem Finset.Nonempty.div_zero {α : Type u_1} [GroupWithZero α] [DecidableEq α] {s : Finset α} (hs : s.Nonempty) : s / 0 = 0

theorem Finset.Nonempty.zero_div {α : Type u_1} [GroupWithZero α] [DecidableEq α] {s : Finset α} (hs : s.Nonempty) : 0 / s = 0

@[simp]

theorem Finset.inv_zero {α : Type u_1} [GroupWithZero α] [DecidableEq α] : 0⁻¹ = 0