equal
deleted
inserted
replaced
145 apply (induct "n") |
145 apply (induct "n") |
146 apply (auto simp add: power_Suc zero_neq_one [THEN not_sym]) |
146 apply (auto simp add: power_Suc zero_neq_one [THEN not_sym]) |
147 done |
147 done |
148 |
148 |
149 lemma field_power_eq_0_iff [simp]: |
149 lemma field_power_eq_0_iff [simp]: |
150 "(a^n = 0) = (a = (0::'a::{field,recpower}) & 0<n)" |
150 "(a^n = 0) = (a = (0::'a::{division_ring,recpower}) & 0<n)" |
151 apply (induct "n") |
151 apply (induct "n") |
152 apply (auto simp add: power_Suc field_mult_eq_0_iff zero_neq_one[THEN not_sym]) |
152 apply (auto simp add: power_Suc field_mult_eq_0_iff zero_neq_one[THEN not_sym]) |
153 done |
153 done |
154 |
154 |
155 lemma field_power_not_zero: "a \<noteq> (0::'a::{field,recpower}) ==> a^n \<noteq> 0" |
155 lemma field_power_not_zero: "a \<noteq> (0::'a::{division_ring,recpower}) ==> a^n \<noteq> 0" |
156 by force |
156 by force |
157 |
157 |
158 lemma nonzero_power_inverse: |
158 lemma nonzero_power_inverse: |
159 "a \<noteq> 0 ==> inverse ((a::'a::{field,recpower}) ^ n) = (inverse a) ^ n" |
159 "a \<noteq> 0 ==> inverse ((a::'a::{division_ring,recpower}) ^ n) = (inverse a) ^ n" |
160 apply (induct "n") |
160 apply (induct "n") |
161 apply (auto simp add: power_Suc nonzero_inverse_mult_distrib mult_commute) |
161 apply (auto simp add: power_Suc nonzero_inverse_mult_distrib power_commutes) |
162 done |
162 done |
163 |
163 |
164 text{*Perhaps these should be simprules.*} |
164 text{*Perhaps these should be simprules.*} |
165 lemma power_inverse: |
165 lemma power_inverse: |
166 "inverse ((a::'a::{field,division_by_zero,recpower}) ^ n) = (inverse a) ^ n" |
166 "inverse ((a::'a::{field,division_by_zero,recpower}) ^ n) = (inverse a) ^ n" |