feat(data/list/basic): add list.prod_eq_zero(_iff) (#6504)

API changes:

* add `list.prod_eq_zero`, `list.prod_eq_zero_iff`, ;
* lemmas `list.prod_ne_zero`, `multiset.prod_ne_zero`, `polynomial.root_list_prod`, `polynomial.roots_multiset_prod`, `polynomial.nat_degree_multiset_prod`,  now assume `0 ∉ L` (or `0 ∉ m`/`0 ∉ s`) instead of `∀ x ∈ L, x ≠ 0`

src/data/list/basic.lean

@@ -2170,10 +2170,33 @@ calc (l₁ ++ l₂).prod = foldl (*) (foldl (*) 1 l₁ * 1) l₂ : by simp [list
 theorem prod_join {l : list (list α)} : l.join.prod = (l.map list.prod).prod :=
 by induction l; [refl, simp only [*, list.join, map, prod_append, prod_cons]]
 
-theorem prod_ne_zero {R : Type*} [domain R] {L : list R} :
-  (∀ x ∈ L, (x : _) ≠ 0) → L.prod ≠ 0 :=
-list.rec_on L (λ _, one_ne_zero) $ λ hd tl ih H,
-  by { rw forall_mem_cons at H, rw prod_cons, exact mul_ne_zero H.1 (ih H.2) }
+/-- If zero is an element of a list `L`, then `list.prod L = 0`. If the domain is a nontrivial
+monoid with zero with no divisors, then this implication becomes an `iff`, see
+`list.prod_eq_zero_iff`. -/
+theorem prod_eq_zero {M₀ : Type*} [monoid_with_zero M₀] {L : list M₀} (h : (0 : M₀) ∈ L) :
+  L.prod = 0 :=
+begin
+  induction L with a L ihL,
+  { exact absurd h (not_mem_nil _) },
+  { rw prod_cons,
+    cases (mem_cons_iff _ _ _).1 h with ha hL,
+    exacts [mul_eq_zero_of_left ha.symm _, mul_eq_zero_of_right _ (ihL hL)] }
+end
+
+/-- Product of elements of a list `L` equals zero if and only if `0 ∈ L`. See also
+`list.prod_eq_zero` for an implication that needs weaker typeclass assumptions. -/
+@[simp] theorem prod_eq_zero_iff {M₀ : Type*} [monoid_with_zero M₀] [nontrivial M₀]
+  [no_zero_divisors M₀] {L : list M₀} :
+  L.prod = 0 ↔ (0 : M₀) ∈ L :=
+begin
+  induction L with a L ihL,
+  { simp },
+  { rw [prod_cons, mul_eq_zero, ihL, mem_cons_iff, eq_comm] }
+end
+
+theorem prod_ne_zero {M₀ : Type*} [monoid_with_zero M₀] [nontrivial M₀] [no_zero_divisors M₀]
+  {L : list M₀} (hL : (0 : M₀) ∉ L) : L.prod ≠ 0 :=
+mt prod_eq_zero_iff.1 hL
 
 @[to_additive]
 theorem prod_eq_foldr : l.prod = foldr (*) 1 l :=

src/data/multiset/basic.lean

@@ -833,19 +833,22 @@ lemma sum_map_mul_right [semiring β] {b : β} {s : multiset α} {f : α → β}
   sum (s.map (λa, f a * b)) = sum (s.map f) * b :=
 multiset.induction_on s (by simp) (assume a s ih, by simp [ih, add_mul])
 
-theorem prod_ne_zero {R : Type*} [comm_semiring R] [no_zero_divisors R] [nontrivial R]
-  {m : multiset R} :
-  (∀ x ∈ m, (x : _) ≠ 0) → m.prod ≠ 0 :=
-multiset.induction_on m (λ _, one_ne_zero) $ λ hd tl ih H,
-  by { rw forall_mem_cons at H, rw prod_cons, exact mul_ne_zero H.1 (ih H.2) }
-
-lemma prod_eq_zero {α : Type*} [comm_semiring α] {s : multiset α} (h : (0 : α) ∈ s) :
+lemma prod_eq_zero {M₀ : Type*} [comm_monoid_with_zero M₀] {s : multiset M₀} (h : (0 : M₀) ∈ s) :
   multiset.prod s = 0 :=
 begin
   rcases multiset.exists_cons_of_mem h with ⟨s', hs'⟩,
   simp [hs', multiset.prod_cons]
 end
 
+lemma prod_eq_zero_iff {M₀ : Type*} [comm_monoid_with_zero M₀] [no_zero_divisors M₀] [nontrivial M₀]
+  {s : multiset M₀} :
+  multiset.prod s = 0 ↔ (0 : M₀) ∈ s :=
+by { rcases s with ⟨l⟩, simp }
+
+theorem prod_ne_zero {M₀ : Type*} [comm_monoid_with_zero M₀] [no_zero_divisors M₀] [nontrivial M₀]
+  {m : multiset M₀} (h : (0 : M₀) ∉ m) : m.prod ≠ 0 :=
+mt prod_eq_zero_iff.1 h
+
 @[to_additive]
 lemma prod_hom [comm_monoid α] [comm_monoid β] (s : multiset α) (f : α →* β) :
   (s.map f).prod = f s.prod :=
@@ -868,12 +871,6 @@ begin
   simp,
 end
 
-theorem prod_eq_zero_iff [comm_cancel_monoid_with_zero α] [nontrivial α]
-  {s : multiset α} :
-  s.prod = 0 ↔ (0 : α) ∈ s :=
-multiset.induction_on s (by simp) $
-  assume a s, by simp [mul_eq_zero, @eq_comm _ 0 a] {contextual := tt}
-
 @[to_additive sum_nonneg]
 lemma one_le_prod_of_one_le [ordered_comm_monoid α] {m : multiset α} :
   (∀ x ∈ m, (1 : α) ≤ x) → 1 ≤ m.prod :=

src/data/polynomial/degree/definitions.lean

@@ -862,6 +862,10 @@ mt degree_eq_bot.2 (show degree ((X : polynomial R) ^ n - C a) ≠ ⊥,
 theorem X_sub_C_ne_zero (r : R) : X - C r ≠ 0 :=
 pow_one (X : polynomial R) ▸ X_pow_sub_C_ne_zero zero_lt_one r
 
+theorem zero_nmem_multiset_map_X_sub_C {α : Type*} (m : multiset α) (f : α → R) :
+  (0 : polynomial R) ∉ m.map (λ a, X - C (f a)) :=
+λ mem, let ⟨a, _, ha⟩ := multiset.mem_map.mp mem in X_sub_C_ne_zero _ ha
+
 lemma nat_degree_X_pow_sub_C {n : ℕ} (hn : 0 < n) {r : R} :
   (X ^ n - C r).nat_degree = n :=
 by { apply nat_degree_eq_of_degree_eq_some, simp [degree_X_pow_sub_C hn], }

src/data/polynomial/ring_division.lean

@@ -355,32 +355,23 @@ by rw [count_roots h, count_zero, root_multiplicity_eq_zero not_root]
 roots_C 1
 
 lemma roots_list_prod (L : list (polynomial R)) :
-  (∀ p ∈ L, (p : _) ≠ 0) → L.prod.roots = (L : multiset (polynomial R)).bind roots :=
+  ((0 : polynomial R) ∉ L) → L.prod.roots = (L : multiset (polynomial R)).bind roots :=
 list.rec_on L (λ _, roots_one) $ λ hd tl ih H,
 begin
-  rw list.forall_mem_cons at H,
-  rw [list.prod_cons, roots_mul (mul_ne_zero H.1 $ list.prod_ne_zero H.2),
+  rw [list.mem_cons_iff, not_or_distrib] at H,
+  rw [list.prod_cons, roots_mul (mul_ne_zero (ne.symm H.1) $ list.prod_ne_zero H.2),
       ← multiset.cons_coe, multiset.cons_bind, ih H.2]
 end
 
 lemma roots_multiset_prod (m : multiset (polynomial R)) :
-  (∀ p ∈ m, (p : _) ≠ 0) → m.prod.roots = m.bind roots :=
-multiset.induction_on m (λ _, roots_one) $ λ hd tl ih H,
-begin
-  rw multiset.forall_mem_cons at H,
-  rw [multiset.prod_cons, roots_mul (mul_ne_zero H.1 $ multiset.prod_ne_zero H.2),
-      multiset.cons_bind, ih H.2]
-end
+  (0 : polynomial R) ∉ m → m.prod.roots = m.bind roots :=
+by { rcases m with ⟨L⟩, simpa only [coe_prod, quot_mk_to_coe''] using roots_list_prod L }
 
 lemma roots_prod {ι : Type*} (f : ι → polynomial R) (s : finset ι) :
   s.prod f ≠ 0 → (s.prod f).roots = s.val.bind (λ i, roots (f i)) :=
 begin
-  refine s.induction_on _ _,
-  { intros, exact roots_one },
-  intros i s hi ih ne_zero,
-  rw prod_insert hi at ⊢ ne_zero,
-  rw [roots_mul ne_zero, ih (right_ne_zero_of_mul ne_zero), insert_val,
-      ndinsert_of_not_mem hi, cons_bind]
+  rcases s with ⟨m, hm⟩,
+  simpa [multiset.prod_eq_zero_iff, bind_map] using roots_multiset_prod (m.map f)
 end
 
 lemma roots_prod_X_sub_C (s : finset R) :

src/field_theory/splitting_field.lean

@@ -196,10 +196,10 @@ theorem roots_map {f : polynomial α} (hf : f.splits $ ring_hom.id α) :
 if hf0 : f = 0 then by rw [hf0, map_zero, roots_zero, roots_zero, multiset.map_zero] else
 have hmf0 : f.map i ≠ 0 := map_ne_zero hf0,
 let ⟨m, hm⟩ := exists_multiset_of_splits _ hf in
-have h1 : ∀ p ∈ m.map (λ r, X - C r), (p : _) ≠ 0,
-  from multiset.forall_mem_map_iff.2 $ λ _ _, X_sub_C_ne_zero _,
-have h2 : ∀ p ∈ m.map (λ r, X - C (i r)), (p : _) ≠ 0,
-  from multiset.forall_mem_map_iff.2 $ λ _ _, X_sub_C_ne_zero _,
+have h1 : (0 : polynomial α) ∉ m.map (λ r, X - C r),
+  from zero_nmem_multiset_map_X_sub_C _ _,
+have h2 : (0 : polynomial β) ∉ m.map (λ r, X - C (i r)),
+  from zero_nmem_multiset_map_X_sub_C _ _,
 begin
   rw map_id at hm, rw hm at hf0 hmf0 ⊢, rw map_mul at hmf0 ⊢,
   rw [roots_mul hf0, roots_mul hmf0, map_C, roots_C, zero_add, roots_C, zero_add,
@@ -223,18 +223,16 @@ begin
   have prod_ne_zero : C (i p.leading_coeff) * (multiset.map (λ a, X - C a) s).prod ≠ 0 :=
     by rwa hs at map_ne_zero,
 
-  have ne_zero_of_mem : ∀ (p : polynomial β), p ∈ s.map (λ a, X - C a) → p ≠ 0,
-  { intros p mem,
-    obtain ⟨a, _, rfl⟩ := multiset.mem_map.mp mem,
-    apply X_sub_C_ne_zero },
+  have zero_nmem : (0 : polynomial β) ∉ s.map (λ a, X - C a),
+    from zero_nmem_multiset_map_X_sub_C _ _,
   have map_bind_roots_eq : (s.map (λ a, X - C a)).bind (λ a, a.roots) = s,
   { refine multiset.induction_on s (by rw [multiset.map_zero, multiset.zero_bind]) _,
     intros a s ih,
     rw [multiset.map_cons, multiset.cons_bind, ih, roots_X_sub_C,
         multiset.cons_add, zero_add] },
 
   rw [hs, roots_mul prod_ne_zero, roots_C, zero_add,
-      roots_multiset_prod _ ne_zero_of_mem,
+      roots_multiset_prod _ zero_nmem,
       map_bind_roots_eq]
 end
 
@@ -247,17 +245,17 @@ begin
 end
 
 lemma nat_degree_multiset_prod {R : Type*} [integral_domain R] {s : multiset (polynomial R)}
-  (h : ∀ p ∈ s, p ≠ (0 : polynomial R)) :
+  (h : (0 : polynomial R) ∉ s) :
   nat_degree s.prod = (s.map nat_degree).sum :=
 begin
   revert h,
   refine s.induction_on _ _,
   { simp },
   intros p s ih h,
-  have hs : ∀ p ∈ s, p ≠ (0 : polynomial R) := λ p hp, h p (multiset.mem_cons_of_mem hp),
-  have hprod : s.prod ≠ 0 := multiset.prod_ne_zero (λ p hp, hs p hp),
-  rw [multiset.prod_cons, nat_degree_mul (h p (multiset.mem_cons_self _ _)) hprod, ih hs,
-      multiset.map_cons, multiset.sum_cons],
+  rw [multiset.mem_cons, not_or_distrib] at h,
+  have hprod : s.prod ≠ 0 := multiset.prod_ne_zero h.2,
+  rw [multiset.prod_cons, nat_degree_mul (ne.symm h.1) hprod, ih h.2,
+    multiset.map_cons, multiset.sum_cons],
 end
 
 lemma nat_degree_eq_card_roots {p : polynomial α} {i : α →+* β}
@@ -269,10 +267,8 @@ begin
   rw eq_prod_roots_of_splits hsplit at map_ne_zero,
 
   conv_lhs { rw [← nat_degree_map i, eq_prod_roots_of_splits hsplit] },
-  have : ∀ p' ∈ (map i p).roots.map (λ a, X - C a), p' ≠ (0 : polynomial β),
-  { intros p hp,
-    obtain ⟨a, ha, rfl⟩ := multiset.mem_map.mp hp,
-    exact X_sub_C_ne_zero _ },
+  have : (0 : polynomial β) ∉ (map i p).roots.map (λ a, X - C a),
+    from zero_nmem_multiset_map_X_sub_C _ _,
   simp [nat_degree_mul (left_ne_zero_of_mul map_ne_zero) (right_ne_zero_of_mul map_ne_zero),
         nat_degree_multiset_prod this]
 end
@@ -349,13 +345,9 @@ begin
   { simp only [prod_multiset_root_eq_finset_root (ne_zero_of_monic hmonic),
       monic_prod_of_monic, monic_X_sub_C, monic_pow, forall_true_iff] },
   have hdegree : (multiset.map (λ (a : α), X - C a) p.roots).prod.nat_degree = p.nat_degree,
-  { rw [← hroots, nat_degree_multiset_prod],
+  { rw [← hroots, nat_degree_multiset_prod (zero_nmem_multiset_map_X_sub_C _ (λ a : α, a))],
     simp only [eq_self_iff_true, mul_one, nat.cast_id, nsmul_eq_mul, multiset.sum_repeat,
-      multiset.map_const,nat_degree_X_sub_C, function.comp, multiset.map_map],
-    intros x y,
-    simp only [multiset.mem_map] at y,
-    rcases y with ⟨a, ha, rfl⟩,
-    exact X_sub_C_ne_zero a },
+      multiset.map_const,nat_degree_X_sub_C, function.comp, multiset.map_map] },
   obtain ⟨q, hq⟩ := prod_multiset_X_sub_C_dvd p,
   have qzero : q ≠ 0,
   { rintro rfl, apply hmonic.ne_zero, simpa only [mul_zero] using hq },