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