# HG changeset patch # User huffman # Date 1179384837 -7200 # Node ID f6b8184f5b4afc0f65d3eaa5eee224e03223cfff # Parent 550709aa8e66d4d36020ffcbb4a46e55a1251bec generalize some lemmas from field to division_ring diff -r 550709aa8e66 -r f6b8184f5b4a src/HOL/Power.thy --- a/src/HOL/Power.thy Thu May 17 08:42:51 2007 +0200 +++ b/src/HOL/Power.thy Thu May 17 08:53:57 2007 +0200 @@ -147,18 +147,18 @@ done lemma field_power_eq_0_iff [simp]: - "(a^n = 0) = (a = (0::'a::{field,recpower}) & 0 (0::'a::{field,recpower}) ==> a^n \ 0" +lemma field_power_not_zero: "a \ (0::'a::{division_ring,recpower}) ==> a^n \ 0" by force lemma nonzero_power_inverse: - "a \ 0 ==> inverse ((a::'a::{field,recpower}) ^ n) = (inverse a) ^ n" + "a \ 0 ==> inverse ((a::'a::{division_ring,recpower}) ^ n) = (inverse a) ^ n" apply (induct "n") -apply (auto simp add: power_Suc nonzero_inverse_mult_distrib mult_commute) +apply (auto simp add: power_Suc nonzero_inverse_mult_distrib power_commutes) done text{*Perhaps these should be simprules.*}