src/HOL/IntDiv.thy
changeset 24391 b57c48f7e2d4
parent 24286 7619080e49f0
child 24481 c3a4a289decc
     1.1 --- a/src/HOL/IntDiv.thy	Tue Aug 21 20:50:12 2007 +0200
     1.2 +++ b/src/HOL/IntDiv.thy	Tue Aug 21 20:51:10 2007 +0200
     1.3 @@ -1357,6 +1357,9 @@
     1.4    show "z^(Suc n) = z * (z^n)" by simp
     1.5  qed
     1.6  
     1.7 +lemma of_int_power:
     1.8 +  "of_int (z ^ n) = (of_int z ^ n :: 'a::{recpower, ring_1})"
     1.9 +  by (induct n) (simp_all add: power_Suc)
    1.10  
    1.11  lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
    1.12  apply (induct "y", auto)