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