src/HOL/Power.thy
 changeset 22988 f6b8184f5b4a parent 22957 82a799ae7579 child 22991 b9e2a133e84e
```     1.1 --- a/src/HOL/Power.thy	Thu May 17 08:42:51 2007 +0200
1.2 +++ b/src/HOL/Power.thy	Thu May 17 08:53:57 2007 +0200
1.3 @@ -147,18 +147,18 @@
1.4  done
1.5
1.6  lemma field_power_eq_0_iff [simp]:
1.7 -     "(a^n = 0) = (a = (0::'a::{field,recpower}) & 0<n)"
1.8 +     "(a^n = 0) = (a = (0::'a::{division_ring,recpower}) & 0<n)"
1.9  apply (induct "n")
1.10  apply (auto simp add: power_Suc field_mult_eq_0_iff zero_neq_one[THEN not_sym])
1.11  done
1.12
1.13 -lemma field_power_not_zero: "a \<noteq> (0::'a::{field,recpower}) ==> a^n \<noteq> 0"
1.14 +lemma field_power_not_zero: "a \<noteq> (0::'a::{division_ring,recpower}) ==> a^n \<noteq> 0"
1.15  by force
1.16
1.17  lemma nonzero_power_inverse:
1.18 -  "a \<noteq> 0 ==> inverse ((a::'a::{field,recpower}) ^ n) = (inverse a) ^ n"
1.19 +  "a \<noteq> 0 ==> inverse ((a::'a::{division_ring,recpower}) ^ n) = (inverse a) ^ n"
1.20  apply (induct "n")
1.21 -apply (auto simp add: power_Suc nonzero_inverse_mult_distrib mult_commute)
1.22 +apply (auto simp add: power_Suc nonzero_inverse_mult_distrib power_commutes)
1.23  done
1.24
1.25  text{*Perhaps these should be simprules.*}
```