src/HOL/Power.thy
changeset 56481 47500d0881f9
parent 56480 093ea91498e6
child 56536 aefb4a8da31f
equal deleted inserted replaced
56480:093ea91498e6 56481:47500d0881f9
   659 
   659 
   660 lemma power_one_over:
   660 lemma power_one_over:
   661   "1 / (a::'a::{field_inverse_zero, power}) ^ n =  (1 / a) ^ n"
   661   "1 / (a::'a::{field_inverse_zero, power}) ^ n =  (1 / a) ^ n"
   662   by (simp add: divide_inverse) (rule power_inverse)
   662   by (simp add: divide_inverse) (rule power_inverse)
   663 
   663 
   664 lemma power_divide [field_simps]:
   664 lemma power_divide [field_simps, divide_simps]:
   665   "(a / b) ^ n = (a::'a::field_inverse_zero) ^ n / b ^ n"
   665   "(a / b) ^ n = (a::'a::field_inverse_zero) ^ n / b ^ n"
   666 apply (cases "b = 0")
   666 apply (cases "b = 0")
   667 apply (simp add: power_0_left)
   667 apply (simp add: power_0_left)
   668 apply (rule nonzero_power_divide)
   668 apply (rule nonzero_power_divide)
   669 apply assumption
   669 apply assumption