Integer factorisations of 2

A nonnegative (resp. nonpositive) integer whose product with another integer is 2 is 1 or 2 (resp. -1 or -2), and the cofactor is the other one.

Main results

• Int.eq_one_and_eq_two_or_of_mul_eq_two: the two ordered factorisations of 2 by a nonnegative first factor.
• Int.eq_neg_one_and_eq_neg_two_or_of_mul_eq_two: the same for a nonpositive first factor.

theorem Int.eq_one_and_eq_two_or_of_mul_eq_two {a b : ℤ} (ha : 0 ≤ a) (hab : a * b = 2) : a = 1 ∧ b = 2 ∨ a = 2 ∧ b = 1

A nonnegative integer factor of 2 is 1 or 2: if a * b = 2 and 0 ≤ a, then (a, b) is (1, 2) or (2, 1).

theorem Int.eq_neg_one_and_eq_neg_two_or_of_mul_eq_two {x y : ℤ} (hx : x ≤ 0) (hxy : x * y = 2) : x = -1 ∧ y = -2 ∨ x = -2 ∧ y = -1

Two nonpositive integers whose product is 2 are -1 and -2, in one order or the other: if x ≤ 0 and x * y = 2, then (x, y) is (-1, -2) or (-2, -1).