equal
deleted
inserted
replaced
330 "abs (a ^ n) = abs a ^ n" |
330 "abs (a ^ n) = abs a ^ n" |
331 by (induct n) (auto simp add: abs_mult) |
331 by (induct n) (auto simp add: abs_mult) |
332 |
332 |
333 lemma abs_power_minus [simp]: |
333 lemma abs_power_minus [simp]: |
334 "abs ((-a) ^ n) = abs (a ^ n)" |
334 "abs ((-a) ^ n) = abs (a ^ n)" |
335 by (simp add: abs_minus_cancel power_abs) |
335 by (simp add: power_abs) |
336 |
336 |
337 lemma zero_less_power_abs_iff [simp, noatp]: |
337 lemma zero_less_power_abs_iff [simp, noatp]: |
338 "0 < abs a ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0" |
338 "0 < abs a ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0" |
339 proof (induct n) |
339 proof (induct n) |
340 case 0 show ?case by simp |
340 case 0 show ?case by simp |