src/HOL/Int.thy

--- a/src/HOL/Int.thy	Sun Sep 17 18:56:35 2023 +0100
+++ b/src/HOL/Int.thy	Sat Sep 23 18:45:19 2023 +0100
@@ -1487,6 +1487,9 @@
     using pos_zmult_eq_1_iff_lemma [OF L] L by force
 qed auto
 
+lemma zmult_eq_neg1_iff: "a * b = (-1 :: int) \<longleftrightarrow> a = 1 \<and> b = -1 \<or> a = -1 \<and> b = 1"
+  using zmult_eq_1_iff[of a "-b"] by auto
+
 lemma infinite_UNIV_int [simp]: "\<not> finite (UNIV::int set)"
 proof
   assume "finite (UNIV::int set)"