changeset 30730 | 4d3565f2cb0e |
parent 30516 | 68b4a06cbd5c |
child 30960 | fec1a04b7220 |
--- a/src/HOL/Power.thy Wed Mar 25 14:47:08 2009 +0100 +++ b/src/HOL/Power.thy Thu Mar 26 14:10:48 2009 +0000 @@ -186,6 +186,10 @@ apply (auto simp add: abs_mult) done +lemma abs_power_minus [simp]: + fixes a:: "'a::{ordered_idom,recpower}" shows "abs((-a) ^ n) = abs(a ^ n)" + by (simp add: abs_minus_cancel power_abs) + lemma zero_less_power_abs_iff [simp,noatp]: "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_idom,recpower}) | n=0)" proof (induct "n")