Commit 2022-11-13 17:27 2181b224

feat(data/int/basic): add lemmas for w*z = -1 (#17478) This small PR adds two lemmas:

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

that are analogous to the existing eq_one_or_neg_one_of_mul_eq_one and eq_one_or_neg_one_of_mul_eq_one'. On request by Eric Wieser, this also adds

lemma mul_eq_neg_one_iff_eq_one_or_neg_one {z w : ℤ} : z * w = -1 ↔ z = 1 ∧ w = -1 ∨ z = -1 ∧ w = 1

and its analogue

lemma mul_eq_one_iff_eq_one_or_neg_one {z w : ℤ} : z * w = 1 ↔ z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1