feat(data/finset/basic): empty_product and product_empty (#7886)

add `product_empty_<left/right>`

Author: YaelDillies

src/data/finset/basic.lean

@@ -2580,7 +2580,7 @@ theorem subset_product [decidable_eq α] [decidable_eq β] {s : finset (α × β
 λ p hp, mem_product.2 ⟨mem_image_of_mem _ hp, mem_image_of_mem _ hp⟩
 
 theorem product_eq_bUnion [decidable_eq α] [decidable_eq β] (s : finset α) (t : finset β) :
- s.product t = s.bUnion (λa, t.image $ λb, (a, b)) :=
+  s.product t = s.bUnion (λa, t.image $ λb, (a, b)) :=
 ext $ λ ⟨x, y⟩, by simp only [mem_product, mem_bUnion, mem_image, exists_prop, prod.mk.inj_iff,
   and.left_comm, exists_and_distrib_left, exists_eq_right, exists_eq_left]
 
@@ -2603,6 +2603,14 @@ begin
   { rw disjoint_iff, change _ ∩ _ = ∅, ext ⟨a, b⟩, rw mem_inter, finish, },
 end
 
+lemma empty_product (t : finset β) :
+  (∅ : finset α).product t = ∅ :=
+rfl
+
+lemma product_empty (s : finset α) :
+  s.product (∅ : finset β) = ∅ :=
+eq_empty_of_forall_not_mem (λ x h, (finset.mem_product.1 h).2)
+
 end prod
 
 /-! ### sigma -/