131 apply (auto simp add: mult_strict_mono zero_le_power power_Suc |
131 apply (auto simp add: mult_strict_mono zero_le_power power_Suc |
132 order_le_less_trans [of 0 a b]) |
132 order_le_less_trans [of 0 a b]) |
133 done |
133 done |
134 |
134 |
135 lemma power_eq_0_iff [simp]: |
135 lemma power_eq_0_iff [simp]: |
136 "(a^n = 0) = (a = (0::'a::{dom,recpower}) & 0<n)" |
136 "(a^n = 0) = (a = (0::'a::{ring_1_no_zero_divisors,recpower}) & 0<n)" |
137 apply (induct "n") |
137 apply (induct "n") |
138 apply (auto simp add: power_Suc zero_neq_one [THEN not_sym]) |
138 apply (auto simp add: power_Suc zero_neq_one [THEN not_sym]) |
139 done |
139 done |
140 |
140 |
141 lemma field_power_eq_0_iff: |
141 lemma field_power_eq_0_iff: |
142 "(a^n = 0) = (a = (0::'a::{division_ring,recpower}) & 0<n)" |
142 "(a^n = 0) = (a = (0::'a::{division_ring,recpower}) & 0<n)" |
143 by simp (* TODO: delete *) |
143 by simp (* TODO: delete *) |
144 |
144 |
145 lemma field_power_not_zero: "a \<noteq> (0::'a::{dom,recpower}) ==> a^n \<noteq> 0" |
145 lemma field_power_not_zero: "a \<noteq> (0::'a::{ring_1_no_zero_divisors,recpower}) ==> a^n \<noteq> 0" |
146 by force |
146 by force |
147 |
147 |
148 lemma nonzero_power_inverse: |
148 lemma nonzero_power_inverse: |
149 fixes a :: "'a::{division_ring,recpower}" |
149 fixes a :: "'a::{division_ring,recpower}" |
150 shows "a \<noteq> 0 ==> inverse (a ^ n) = (inverse a) ^ n" |
150 shows "a \<noteq> 0 ==> inverse (a ^ n) = (inverse a) ^ n" |