Product of integers is -1 [title changed]

Stream: Is there code for X?

[Michael Stoll]

lemma int_prod_eq_neg_one' {l : list ℤ} (h : l.prod = -1) : (-1 : ℤ) ∈ l :=
begin
  induction l with n l',
  { rw [prod_nil] at h,
    exact false.elim ((dec_trivial : ¬ (1 : ℤ) = -1) h), },
  rw [prod_cons, eq_neg_iff_eq_neg, ← mul_neg] at h,
  rcases int.eq_one_or_neg_one_of_mul_eq_one' h.symm with (⟨_, h₂⟩ | ⟨rfl, h₂⟩),
  { exact mem_cons_of_mem _ (l_ih (neg_eq_iff_neg_eq.mp h₂).symm), },
  { exact mem_cons_self _ _, }
end

This would be a bit easier if we had

lemma int.eq_one_or_neg_one_of_mul_eq_neg_one' {z w : ℤ} (h : z * w = -1) :
z = 1 ∧ w = -1 ∨ z = -1 ∧ w = 1

in addition to docs#int.eq_one_or_neg_one_of_mul_eq_one'.

[Michael Stoll]

I have made a PR (#17478) that adds int.eq_one_or_neg_one_of_mul_eq_neg_one' (and the one-sided version int.eq_one_or_neg_one_of_mul_eq_neg_one). I think this is useful to have, and it should be quick to review.

[Joseph Myers]

I think the lemma you have as int_prod_eq_neg_one' is appropriate for mathlib. My inclination would be to deduce it from two more general lemmas: in any monoid, if a product is not 1, it has some term that is not 1; and in any commutative monoid, if a product is a unit, all terms of the product are units. (And then combine those with the only two units of the integers being 1 and -1.)

[Yaël Dillies]

The second one is basically monotonicity of being a unit under division.

[Michael Stoll]

Joseph Myers said:

I think the lemma you have as int_prod_eq_neg_one' is appropriate for mathlib. My inclination would be to deduce it from two more general lemmas: in any monoid, if a product is not 1, it has some term that is not 1; and in any commutative monoid, if a product is a unit, all terms of the product are units. (And then combine those with the only two units of the integers being 1 and -1.)

OK, I'll do that. I assume this should go into file#data/list/big_operators ?

[Michael Stoll]

#17499