neg_one_mem_of_prod_eq_neg_one — Mathlib

English

If the product of a finite list of integers is −1, then the value −1 must appear among the factors.

Русский

Если произведение конечного списка целых чисел равно −1, тогда среди множителей обязательно встречается −1.

LaTeX

$$$$ l.prod = -1 \implies (-1) \in l. $$$$

Lean4

/-- If a product of integers is `-1`, then at least one factor must be `-1`. -/
theorem neg_one_mem_of_prod_eq_neg_one {l : List ℤ} (h : l.prod = -1) : (-1 : ℤ) ∈ l :=
  by
  obtain ⟨x, h₁, h₂⟩ := exists_mem_ne_one_of_prod_ne_one (ne_of_eq_of_ne h (by decide))
  exact
    Or.resolve_left
        (Int.isUnit_iff.mp (prod_isUnit_iff.mp (h.symm ▸ ⟨⟨-1, -1, by decide, by decide⟩, rfl⟩ : IsUnit l.prod) x h₁))
        h₂ ▸
      h₁

Похожие утверждения