chore(algebra/big_operators): use proper *_with_zero class in `prod…

…_eq_zero(_iff)` (#3303)

Also add a missing instance `comm_semiring → comm_monoid_with_zero`.

src/algebra/big_operators.lean

@@ -1111,11 +1111,6 @@ calc (∑ x in s, f x) / b = ∑ x in s, f x * (1 / b) : by rw [div_eq_mul_one_d
 section comm_semiring
 variables [comm_semiring β]
 
-lemma prod_eq_zero (ha : a ∈ s) (h : f a = 0) : (∏ x in s, f x) = 0 :=
-by haveI := classical.dec_eq α;
-calc (∏ x in s, f x) = ∏ x in insert a (erase s a), f x : by rw insert_erase ha
-                 ... = 0 : by rw [prod_insert (not_mem_erase _ _), h, zero_mul]
-
 /-- The product over a sum can be written as a sum over the product of sets, `finset.pi`.
   `finset.prod_univ_sum` is an alternative statement when the product is over `univ`. -/
 lemma prod_sum {δ : α → Type*} [decidable_eq α] [∀a, decidable_eq (δ a)]
@@ -1205,8 +1200,15 @@ end
 
 end comm_semiring
 
-section integral_domain /- add integral_semi_domain to support nat and ennreal -/
-variables [integral_domain β]
+section prod_eq_zero
+variables [comm_monoid_with_zero β]
+
+lemma prod_eq_zero (ha : a ∈ s) (h : f a = 0) : (∏ x in s, f x) = 0 :=
+by haveI := classical.dec_eq α;
+calc (∏ x in s, f x) = ∏ x in insert a (erase s a), f x : by rw insert_erase ha
+                 ... = 0 : by rw [prod_insert (not_mem_erase _ _), h, zero_mul]
+
+variables [nontrivial β] [no_zero_divisors β]
 
 lemma prod_eq_zero_iff : (∏ x in s, f x) = 0 ↔ (∃a∈s, f a = 0) :=
 begin
@@ -1220,7 +1222,7 @@ end
 theorem prod_ne_zero_iff : (∏ x in s, f x) ≠ 0 ↔ (∀ a ∈ s, f a ≠ 0) :=
 by { rw [ne, prod_eq_zero_iff], push_neg }
 
-end integral_domain
+end prod_eq_zero
 
 section ordered_add_comm_monoid
 variables [ordered_add_comm_monoid β]

src/algebra/ring.lean

@@ -338,6 +338,9 @@ instance comm_semiring.to_comm_monoid_with_zero [comm_semiring α] : comm_monoid
 section comm_semiring
 variables [comm_semiring α] [comm_semiring β] {a b c : α}
 
+instance comm_semiring.comm_monoid_with_zero : comm_monoid_with_zero α :=
+{ .. (‹_› : comm_semiring α) }
+
 /-- Pullback a `semiring` instance along an injective function. -/
 protected def function.injective.comm_semiring [has_zero γ] [has_one γ] [has_add γ] [has_mul γ]
   (f : γ → α) (hf : injective f) (zero : f 0 = 0) (one : f 1 = 1)

src/data/support.lean

@@ -27,6 +27,10 @@ lemma nmem_support [has_zero A] {f : α → A} {x : α} :
   x ∉ support f ↔ f x = 0 :=
 classical.not_not
 
+lemma mem_support [has_zero A] {f : α → A} {x : α} :
+  x ∈ support f ↔ f x ≠ 0 :=
+iff.rfl
+
 lemma support_binop_subset [has_zero A] (op : A → A → A) (op0 : op 0 0 = 0) (f g : α → A) :
   support (λ x, op (f x) (g x)) ⊆ support f ∪ support g :=
 λ x hx, classical.by_cases
@@ -98,10 +102,14 @@ begin
   exact finset.sum_eq_zero hx
 end
 
--- TODO: Drop `classical` once #2332 is merged
-lemma support_prod [integral_domain A] (s : finset α) (f : α → β → A) :
+lemma support_prod_subset [comm_monoid_with_zero A] (s : finset α) (f : α → β → A) :
+  support (λ x, ∏ i in s, f i x) ⊆ ⋂ i ∈ s, support (f i) :=
+λ x hx, mem_bInter_iff.2 $ λ i hi H, hx $ finset.prod_eq_zero hi H
+
+lemma support_prod [comm_monoid_with_zero A] [no_zero_divisors A] [nontrivial A]
+  (s : finset α) (f : α → β → A) :
   support (λ x, ∏ i in s, f i x) = ⋂ i ∈ s, support (f i) :=
-set.ext $ λ x, by classical;
+set.ext $ λ x, by
   simp only [support, ne.def, finset.prod_eq_zero_iff, mem_set_of_eq, set.mem_Inter, not_exists]
 
 lemma support_comp [has_zero A] [has_zero B] (g : A → B) (hg : g 0 = 0) (f : α → A) :