src/HOL/Parity.thy

--- a/src/HOL/Parity.thy	Sun Jan 07 22:18:59 2018 +0100
+++ b/src/HOL/Parity.thy	Mon Jan 08 17:11:25 2018 +0000
@@ -483,6 +483,9 @@
 lemma neg_one_power_add_eq_neg_one_power_diff: "k \<le> n \<Longrightarrow> (- 1) ^ (n + k) = (- 1) ^ (n - k)"
   by (cases "even (n + k)") auto
 
+lemma minus_one_power_iff: "(- 1) ^ n = (if even n then 1 else - 1)"
+  by (induct n) auto
+
 end
 
 context linordered_idom