Commit 2022-11-21 23:13 cadea043

feat(data/list/big_operators): add lemmas on products/sums (#17499) This PR adds three lemmas to data.list.big_operators:

@[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

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.