equal
deleted
inserted
replaced
1355 fix n :: nat |
1355 fix n :: nat |
1356 show "z^0 = 1" by simp |
1356 show "z^0 = 1" by simp |
1357 show "z^(Suc n) = z * (z^n)" by simp |
1357 show "z^(Suc n) = z * (z^n)" by simp |
1358 qed |
1358 qed |
1359 |
1359 |
|
1360 lemma of_int_power: |
|
1361 "of_int (z ^ n) = (of_int z ^ n :: 'a::{recpower, ring_1})" |
|
1362 by (induct n) (simp_all add: power_Suc) |
1360 |
1363 |
1361 lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m" |
1364 lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m" |
1362 apply (induct "y", auto) |
1365 apply (induct "y", auto) |
1363 apply (rule zmod_zmult1_eq [THEN trans]) |
1366 apply (rule zmod_zmult1_eq [THEN trans]) |
1364 apply (simp (no_asm_simp)) |
1367 apply (simp (no_asm_simp)) |