Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-03 13:41 d4ac4c3e

View on Github →

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

Estimated changes

added theorem list.prod_eq_zero
added theorem list.prod_eq_zero_iff
modified theorem list.prod_ne_zero
modified theorem multiset.prod_eq_zero
modified theorem multiset.prod_eq_zero_iff
modified theorem multiset.prod_ne_zero