Pointwise operations of finsets in a group with zero

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

theorem Finset.card_le_card_mul_left₀ {α : Type u_1} [Mul α] [Zero α] [DecidableEq α] {s t : Finset α} {a : α} [IsLeftCancelMulZero α] (has : a ∈ s) (ha : a ≠ 0) : t.card ≤ (s * t).card

theorem Finset.card_le_card_mul_right₀ {α : Type u_1} [Mul α] [Zero α] [DecidableEq α] {s t : Finset α} {a : α} [IsRightCancelMulZero α] (hat : a ∈ t) (ha : a ≠ 0) : s.card ≤ (s * t).card

theorem Finset.card_le_card_mul_self₀ {α : Type u_1} [Mul α] [Zero α] [DecidableEq α] {s : Finset α} [IsLeftCancelMulZero α] : s.card ≤ (s * s).card

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