mathlib

cadea043 - feat(data/list/big_operators): add lemmas on products/sums (#17499)

feat(data/list/big_operators): add lemmas on products/sums (#17499) This PR adds three lemmas to `data.list.big_operators`: ```lean @[to_additive] lemma prod_is_unit_iff {α : Type*} [comm_monoid α] {L : list α} : is_unit L.prod ↔ ∀ m ∈ L, is_unit m @[to_additive] lemma exists_mem_ne_one_of_prod_ne_one [monoid M] {l : list M} (h : l.prod ≠ 1) : ∃ (x ∈ l), x ≠ (1 : M) ``` and ```lean lemma neg_one_mem_of_prod_eq_neg_one {l : list ℤ} (h : l.prod = -1) : (-1 : ℤ) ∈ l ``` which is proved using the first two. See this [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Product.20of.20integers.20is.20-1.20.5Btitle.20changed.5D/near/309326756).