src/HOL/Parity.thy
changeset 62083 7582b39f51ed
parent 61799 4cf66f21b764
child 62597 b3f2b8c906a6
     1.1 --- a/src/HOL/Parity.thy	Wed Jan 06 13:04:31 2016 +0100
     1.2 +++ b/src/HOL/Parity.thy	Wed Jan 06 12:18:53 2016 +0100
     1.3 @@ -321,7 +321,10 @@
     1.4      with \<open>a \<le> b\<close> show ?thesis using power_mono by auto
     1.5    qed
     1.6  qed
     1.7 - 
     1.8 +
     1.9 +lemma (in comm_ring_1) uminus_power_if: "(- x) ^ n = (if even n then x^n else - (x ^ n))"
    1.10 +  by auto
    1.11 +
    1.12  text \<open>Simplify, when the exponent is a numeral\<close>
    1.13  
    1.14  lemma zero_le_power_eq_numeral [simp]: